# Complete resolution rule for 1-in-k SAT

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?

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.