In CNF SAT, each clause (A or B or C or...) must contain at least one true literal. The resolution rule applies to pair of clauses who have exactly one opposite literal.

(A or B or C) and (!A or D or E) => (B or C or D or E)

I say that this rule is complete, in the sense that if a formula is unsatisfiable, I can prove it by applying the rule exhaustively (on hard instances, an exponential amount of times) until one empty clause is produced. If a formula has a unique solution, I can apply the rule until every unit clause is produced.

1-in-k SAT is a NP-complete variant where exactly one variable per clause (A,B,C,....)=1 is true. Given a pair of clause with one opposite literal, and no common literal, I can also produce a third one:

(A,B,C)=1 and (!A,D,E)=1 => (B,C,D,E)=1

Question: Is this rule complete for unsatisfiable and uniquely satisfiable 1-in-k formulas?


1 Answer 1


You're treating resolution as if it were a purely syntactic rule. It works that way with traditional CNF clauses because that corresponds with the underlying rule of inference. But a CNF clause with the added restriction of only one literal allowed to be true no longer corresponds to what the resolution rule can be validly applied to.

The Boolean expression $(a \lor b) \land (\lnot{a} \lor \lnot{b}) \land (\lnot{a} \lor b)$ is unsatisfiable as a 1-in-k-SAT formula but naively applying the resolution rule produces $a = false, b = true$ as a (wrong) solution.

  • $\begingroup$ I used the same letters, but never meant to say the two formulas are equivalent. Obviously, it is different problem and different rules. I'm trying to figure out what can be done with clauses in 1-in-k SAT. $\endgroup$
    – d3m4nz3
    Jun 7, 2020 at 22:05
  • $\begingroup$ @d3m4nz3, I'm not sure whether you've appreciated the point made by this answer. If you think you still have a question, but you're considering some different rule for resolution, I suggest posting a new question, and defining the resolution rule you have in mind for 1-in-k-SAT and proving that it never produces an incorrect solution, and show us that definition in the new post. $\endgroup$
    – D.W.
    Jun 7, 2020 at 23:50
  • $\begingroup$ The answer simply misunderstands the meaning of my question. The rule I described for 1-in-k SAT is valid. If there's exactly 1 true literal in (A,B,C) and exactly 1 true literal in (!A,D,E), then there are exactly 2 true literals in (A,!A,B,C,D,E) but since there's exactly 1 true literal in (A,!A) then there must be exactly 1 true literal in (B,C,D,E). I am asking about the completeness of this rule in 1-in-k SAT, in comparison to the completeness of the resolution rule in SAT. $\endgroup$
    – d3m4nz3
    Jun 8, 2020 at 0:03
  • $\begingroup$ If your rule is valid you should be able to apply it to the formula I gave and show that formula unsatisfiable, since it is unsatisfiable as a 1-in-k-SAT formula. $\endgroup$
    – Kyle Jones
    Jun 8, 2020 at 1:45
  • $\begingroup$ Okay, I understand your answer now. I was confused by OR operator and your explanation about inapplicability of rule. But there's another simple reason why the rule is insufficient. Take an unsatisfiable monotone formula, the rule cannot be applied at all. It's not invalid, it's simply incomplete. $\endgroup$
    – d3m4nz3
    Jun 8, 2020 at 3:00

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.