# CircuitSAT to 1-in-3SAT

This question follows Unique 3SAT to Unique 1-in-3SAT

Consider an AND gate such that (A ∧ B) = C. It can be trivially expressed in 3SAT with 4 clauses and no extra variables.

$$(A ∨ B ∨ \overline{C}) \wedge (A ∨ \overline{B} ∨ \overline{C}) \wedge (\overline{A} ∨ B ∨ \overline{C}) \wedge (\overline{A} ∨ \overline{B} ∨ C)$$

| A | B | C |
|---|---|---|
| 0 | 0 | 0 |
| 0 | 0 | 1 | <-- Eliminated by (A ∨ B ∨ !C)
| 0 | 1 | 0 |
| 0 | 1 | 1 | <-- Eliminated by (A ∨ !B ∨ !C)
| 1 | 0 | 0 |
| 1 | 0 | 1 | <-- Eliminated by (!A ∨ B ∨ !C)
| 1 | 1 | 0 | <-- Eliminated by (!A ∨ !B ∨ C)
| 1 | 1 | 1 |


Using the resolution rule, you can even reduce it to 1 clause of size 3 and 2 clauses of size 2.

$$(A ∨ \overline{C}) \wedge (B ∨ \overline{C}) \wedge (\overline{A} ∨ \overline{B} ∨ C)$$

The OR gate is analogous because if (A ∧ B) = C then (!A ∨ !B) = !C. In other words, you just need to flip all the literals.

For the XOR gate, we could express it using 2 ANDs and 1 OR, or 2 ORs and 1 AND, but that would be a waste of space, especially in a circuit with many XORs. In fact, from observing the truth table again, we can do it again with 4 clauses:

$$(A ∨ B ∨ \overline{C}) \wedge (\overline{A} ∨ \overline{B} ∨ \overline{C}) \wedge (\overline{A} ∨ B ∨ C) \wedge (A ∨ \overline{B} ∨ C)$$

Now I want to reduce the circuit to 1-in-3SAT instead of 3SAT.

While a 3SAT clauses states "at least one of the variables is true", a 1-in-3SAT clause states "exactly one variable in this clause is true and the two other are false".

In the previous question, to reduce an AND gate to 1-in-3SAT, Steven introduces 4 new variables D,E,F,G per gate and expresses the gate using four clauses:

$$(A, D, E) \wedge (B, F, G) \wedge (\overline{A}, F, C) \wedge (\overline{B}, D, C)$$

The reduction is parsimonious because D,E,F,G are entirely determined by A,B.

The OR gate can be obtained by flipping A,B,C.

Question:

How can we do the same with XOR ?

The goal is to obtain a list of 1-in-3SAT clauses that ensures that A xor B = C, with as few new variables as possible, such that the values of the new variables are fully determined by A and B.

A trivial solution is to express A xor B using AND/OR gates, ((A ∧ !B) ∨ ( !A ∧ B)), but doing so introduces 14 new variables (3 gates * 4 variables + 2 intermediate output variables) and 12 clauses which makes XOR gates way more expensive than AND/OR gates.

• Such questions can be very hard to answer. – Yuval Filmus May 11 '20 at 11:33
• The optimality question is not the most important and probably very hard to answer. I'm mostly interested in a short equivalent for XOR. – d3m4nz3 May 11 '20 at 12:13
• Can you state the task in a self-contained way? I'm not sure what "do the same with XOR" means, exactly. I'd have to understand the previous, then infer/reverse-engineer exactly what your requirements are. I don't know what all those parentheses are, and I'm not sure what you mean by "less than the obvious solution" - fewer variables, fewer gates, some other metric? Please state the problem carefully and precisely. Also please ask only one question per post. I'm not sure what is meant by your second question. – D.W. May 12 '20 at 3:52
• I made some adjusments. But I think I will have to turn this into a bounty to make it worth the effort. :) – d3m4nz3 May 12 '20 at 8:07
• @d3m4nz3 Unfortunately those changes didn't address my comments / my confusion. Sorry that I am unable to help more. – D.W. May 12 '20 at 22:40