0
$\begingroup$

I have seen numerous ways to reduce CNF-SAT to SS, but is there any way to reduce SS to SAT (or one of its variations)? I have tried researching it, but all it brings up is the (apparently) much more common opposite reduction.

$\endgroup$
  • 1
    $\begingroup$ Are you familiar with Cook's theorem? $\endgroup$ – Yuval Filmus Jul 29 at 0:04
1
$\begingroup$

You can reduce addition to a circuit with XOR, AND, OR gates.

Each element of the sum must first be ANDed with an extra variable that is true if the element belongs to the subset, and false otherwise.

Then the circuit can be trivially reduced to 3-SAT. The clauses are determined by the gates.

For example each AND gate (A & B = C) requires these 4 clauses:

(A | !B | !C)

(!A | B | !C)

(A | B | !C)

(!A | !B | C)

Why? Because:

false & true != true

true & false != true

false & false != true

true & true != false

Each clause eliminates one impossible situation for the gate.

Then if you want the result of the sum to be zero, you add one unit clause for each bit of the result.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.