2
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
1
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\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$
    – user102180
    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$ 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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.