Exactly $1$-in-$3$ SAT ($X_3SAT$) is a variant of the Boolean satisfiability problem. Given a set of clauses, each clause having three literals, is there a set of literals such that each clause contains exactly one literal from this set?

$X_3SAT$ is known to be $NP$-complete. It remains $NP$-Complete even when it is monotone (all literals are positive) and linear (no two clauses share more than one variable in common).

I am interested in finding short, unsatisfiable $X_3SAT$ instances. The shortest monotone linear $X_3SAT$ instance I have found so far is:


I think unsatisfiable monotone linear instances must have at least 4 loops. A loop is a sequence of clauses such that each clause shares one variable with the previous clause in the sequence, a different variable with the next clause, and doesn't share variables with any other clauses. The example above has six length three loops.







I am interested in short unsatisfiable instances. They don't have to be monotone.

  • $\begingroup$ I am not sure what your question is ... but if you are asking if there is a smaller unsatisfiable monotone linear set, then the answer is no: the one you have is the shortest. $\endgroup$ – Bram28 Dec 30 '17 at 3:21
  • $\begingroup$ I am looking for more examples of short unsatisfiable instances. $\endgroup$ – Russell Easterly Dec 30 '17 at 3:41

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.