Complete resolution rule for 1-in-k SAT

Question

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?

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.