[Rule] CircuitSAT to Satisfiability

[zhangjieqingithub]

Source: CircuitSAT
Target: Satisfiability

Motivation:
CircuitSAT is already a formula-family problem in the repository, but it currently has no reduction path into the main SAT branch. Adding CircuitSAT -> Satisfiability connects it to the existing SAT neighborhood, which already reaches MaximumIndependentSet, KColoring, KSatisfiability, and MinimumDominatingSet. It also complements the existing reverse rule Satisfiability -> CircuitSAT.

Reference:
Panagiotis Manolios and Daron Vroon, “Efficient Circuit to CNF Conversion,” in Theory and Applications of Satisfiability Testing – SAT 2007, LNCS 4501, pp. 4–9, Springer, 2007.
PDF: https://www.ccs.neu.edu/home/pete/pub/sat-cnf.pdf
Proceedings: https://link.springer.com/book/10.1007/978-3-540-72788-0

Historical background: Tseitin-style definitional CNF conversion and the Cook/Karp satisfiability framework.

Reduction Algorithm

Notation:

• The source circuit consists of assignments of the form
  (o_1,\dots,o_m = e),
  where each (o_i) is an output variable and (e) is a Boolean expression.
• Let (V_0) be the set of original circuit variables, i.e. all names that occur anywhere in the source CircuitSAT instance.
• First constant-fold the expressions and flatten every n-ary AND, OR, and XOR into binary gates.
• After this preprocessing, introduce one fresh SAT variable (v_\alpha) for each non-leaf subexpression occurrence (\alpha).
• Original circuit variables are reused directly as SAT variables.

Step 1: Preprocess each right-hand side.
For every assignment (o_1,\dots,o_m = e):

• simplify constant subexpressions;
• rewrite n-ary AND, OR, XOR as binary trees;
• name each non-leaf subexpression occurrence by a fresh SAT variable.

Step 2: Encode each gate by definitional CNF.
For each subexpression variable (v_\alpha):

• If (\alpha = \neg a), add
  [
  (\neg v_\alpha \lor \neg a)\ \land\ (v_\alpha \lor a).
  ]

• If (\alpha = a \land b), add
  [
  (\neg v_\alpha \lor a)\ \land\ (\neg v_\alpha \lor b)\ \land\ (v_\alpha \lor \neg a \lor \neg b).
  ]

• If (\alpha = a \lor b), add
  [
  (v_\alpha \lor \neg a)\ \land\ (v_\alpha \lor \neg b)\ \land\ (\neg v_\alpha \lor a \lor b).
  ]

• If (\alpha = a \oplus b), add
  [
  (\neg a \lor \neg b \lor \neg v_\alpha)
  \land
  (a \lor b \lor \neg v_\alpha)
  \land
  (a \lor \neg b \lor v_\alpha)
  \land
  (\neg a \lor b \lor v_\alpha).
  ]

These clauses force each fresh variable to equal the truth value of its subexpression.

Step 3: Connect assignment outputs.
Let (z_e) be the SAT variable corresponding to the root of the right-hand side (e).

For every output (o_i) in the assignment (o_1,\dots,o_m = e), add
[
(\neg o_i \lor z_e)\ \land\ (o_i \lor \neg z_e).
]

If a right-hand side simplifies to a constant:

• (o = \text{true}) becomes the unit clause ((o)),
• (o = \text{false}) becomes the unit clause ((\neg o)).

Step 4: Build the SAT instance.
The target Satisfiability instance uses:

• one SAT variable for every original circuit variable;
• one fresh SAT variable for every non-leaf subexpression occurrence after preprocessing;
• all clauses generated in Steps 2 and 3.

There is no distinguished final-output clause. This matches the repository’s CircuitSAT semantics, where a solution is any assignment satisfying all circuit assignments.

Correctness Sketch

Forward direction:
Given any satisfying assignment of the source circuit, assign every fresh Tseitin variable (v_\alpha) to the truth value of its corresponding subexpression (\alpha). Then every gate-definition clause is satisfied, and every output-equivalence clause is satisfied, so the constructed CNF is satisfiable.

Backward direction:
Given any satisfying assignment of the target CNF, the gate-definition clauses force each fresh variable to equal the truth value of its subexpression, and the output-equivalence clauses force every declared output to equal the value of the corresponding right-hand side expression. Restricting the SAT assignment to the original circuit variables therefore yields an assignment that satisfies every circuit assignment in the source CircuitSAT instance.

Hence the reduction is equisatisfiable.

Size Overhead

Let:

• (n) be the source num_variables,
• (u) be the total number of output occurrences,
• (N_{\neg}, N_{\land}, N_{\lor}, N_{\oplus}) be the numbers of NOT, binary AND, binary OR, and binary XOR subexpression occurrences after constant-folding and binary flattening.

Then the target Satisfiability instance has:

Target metric	Formula
num_vars	(n + N_{\neg} + N_{\land} + N_{\lor} + N_{\oplus})
num_clauses	(2N_{\neg} + 3N_{\land} + 3N_{\lor} + 4N_{\oplus} + 2u)
num_literals	(4N_{\neg} + 7N_{\land} + 7N_{\lor} + 12N_{\oplus} + 4u)

This is linear in total expression-tree size.
Note: the current CircuitSAT model exposes num_variables and num_assignments, but not total expression-tree size, so the implementation will need internal counting logic for these structural quantities. Constant-only assignments contribute only an additive (O(1)) unit-clause term.

Validation Method

• Closed-loop test: reduce CircuitSAT to Satisfiability, solve the SAT instance with brute force, extract the assignment on the original circuit variables, and verify that all source circuit assignments are satisfied.
• Include cases covering:
  • a single NOT gate,
  • nested AND/OR,
  • XOR,
  • multiple assignments chained through intermediate outputs,
  • an unsatisfiable circuit such as a variable constrained to equal its own negation.
• Cross-check the generated clause counts against the structural formulas above.

Example

Source circuit:
[
r = (x \land y) \lor z,\qquad
s = x \oplus r,\qquad
t = \neg s.
]

This uses the repository’s native CircuitSAT semantics: all three assignments must hold simultaneously.

Preprocessing and fresh variables:
Introduce fresh variables

• (a) for ((x \land y)),
• (b) for ((a \lor z)),
• (c) for ((x \oplus r)),
• (d) for ((\neg s)).

The SAT variables are therefore:
[
x,y,z,r,s,t,a,b,c,d.
]

Generated clauses:

For (a \leftrightarrow (x \land y)):
[
(\neg a \lor x),\quad
(\neg a \lor y),\quad
(a \lor \neg x \lor \neg y).
]

For (b \leftrightarrow (a \lor z)):
[
(b \lor \neg a),\quad
(b \lor \neg z),\quad
(\neg b \lor a \lor z).
]

For (r \leftrightarrow b):
[
(\neg r \lor b),\quad
(r \lor \neg b).
]

For (c \leftrightarrow (x \oplus r)):
[
(\neg x \lor \neg r \lor \neg c),\quad
(x \lor r \lor \neg c),\quad
(x \lor \neg r \lor c),\quad
(\neg x \lor r \lor c).
]

For (s \leftrightarrow c):
[
(\neg s \lor c),\quad
(s \lor \neg c).
]

For (d \leftrightarrow (\neg s)):
[
(\neg d \lor \neg s),\quad
(d \lor s).
]

For (t \leftrightarrow d):
[
(\neg t \lor d),\quad
(t \lor \neg d).
]

Clause counts for this example:

• (n = 6) original circuit variables: (x,y,z,r,s,t)
• (N_{\land} = 1), (N_{\lor} = 1), (N_{\oplus} = 1), (N_{\neg} = 1)
• (u = 3) output occurrences: (r,s,t)

So:

• num_vars = 6 + 1 + 1 + 1 + 1 = 10
• num_clauses = 3 + 3 + 4 + 2 + 6 = 18
• num_literals = 7 + 7 + 12 + 4 + 12 = 42

One satisfying assignment:
[
x=1,\ y=1,\ z=0,\ a=1,\ b=1,\ r=1,\ c=0,\ s=0,\ d=1,\ t=1.
]

Restricting back to the original circuit variables gives:
[
x=1,\ y=1,\ z=0,\ r=1,\ s=0,\ t=1,
]
which indeed satisfies all three circuit assignments.

BibTeX

@inproceedings{ManoliosV07,
  author    = {Panagiotis Manolios and Daron Vroon},
  title     = {Efficient Circuit to CNF Conversion},
  booktitle = {Theory and Applications of Satisfiability Testing -- SAT 2007},
  series    = {Lecture Notes in Computer Science},
  volume    = {4501},
  pages     = {4--9},
  year      = {2007},
  publisher = {Springer},
  doi       = {10.1007/978-3-540-72788-0_3}
}