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?