Reducing Circuit-SAT to SAT

This node is the first concrete bridge from the circuit view to the formula view:

source object: Circuit-SAT
target object: SAT
promise: same Yes/No answer after polynomial-time construction

Reduction bridgeBuild one SAT formula for this fixed circuit instance.

Source instance C

four inputs, six gates, one output

n1 = NOT x2 ; g1 = x1 AND n1 ; g2 = x3 OR x4 ; g3 = g1 AND g2 ; g4 = x2 AND x4 ; z = g3 OR g4

flocal gate constraints + final z

Target formula Φ_C

one formula that is satisfiable iff z can be 1

Φ_C = z ∧ (∧_{g in Gates(C)} emit(g)), where emit uses only AND/OR/NOT.

Answer-preservation bridgeShared rows compare circuit output and formula output.

assignment	C(a)	conjunction without z	final Φ_C(â)	note
1010	1	1	1	The circuit output and the reduced formula output agree on this row.
0101	1	1	1	The circuit output and the reduced formula output agree on this row.
0000	0	1	0	All gate constraints are true, but AND z keeps this one rejecting.

For context, the shared fixture is the same source circuit from Circuit-SAT:

A circuit asks whether some switch setting turns the lamp onInputs are switches, gates apply Boolean rules, wires carry bits forward, and z=1 means the output lamp turns on.

switch = input bit1 AND 0 = 01 OR 0 = 1NOT 0 = 1lamp on means output 1

The four input string positions are x1 x2 x3 x4. For example, 1010 means:

x1=1,\; x2=0,\; x3=1,\; x4=0.

Hook problem: same search, different object

Circuit-SAT asks whether a fixed circuit can output z=1 on some input. SAT asks whether a Boolean formula can evaluate to 1 on some assignment.

Both questions are existence questions over four input bits, but SAT takes a formula. So we need an explicit translation that preserves acceptance.

Naive attempt: inline whole formulas

One obvious idea is to expand every gate expression until only input names remain.

Naive inline expansionThis reads `z` and repeatedly substitutes gate RHS terms.

Gate-level substitutions

n1 = NOT x2

g1 = (x1 AND NOT x2)

g2 = (x3 OR x4)

g3 = ((x1 AND NOT x2) AND (x3 OR x4))

g4 = (x2 AND x4)

z = (((x1 AND NOT x2) AND (x3 OR x4)) OR (x2 AND x4))

Fully inlined zz = (((x1 AND NOT x2) AND (x3 OR x4)) OR (x2 AND x4))

This preserves meaning but can duplicate shared subexpressions many times.

That does preserve meaning, but it can duplicate shared subcircuits and hides the size argument.

Why naive expansion is the wrong general move

Fan-out should be a strength of circuits, but full substitution repeats shared logic.

Fan-out duplication snapshotFlattening fan-out by full substitution duplicates large shared subcircuits.

Shared subexpressionh=(a OR b); p=h AND c; q=h AND d; z=p OR qshared sub-expression h used once

Expanded formulaz=((a OR b) AND c) OR ((a OR b) AND d)inline form uses h twice

That is exactly why we avoid substituting into one giant formula before we know the size.

Core invention: local gate variables + local consistency constraints

Give each non-input circuit node a helper variable named by the same gate id:

n1, g1, g2, g3, g4, z.

For each gate, emit one local constraint that forces the helper equal to the gate expression. In the page logic, we keep this split explicit:

blueprint: readable form with <-> (not emitted as-is), and
emit: actual emitted form in AND/OR/NOT only.

Local gate gadgetsEach gate has one helper and two emitted clauses in constant size.

AND gadget

Blueprint: g <-> (u AND v)

Emitted: (NOT g OR (u AND v)) AND (NOT (u AND v) OR g)

Two inputs, one helper variable, constant-size emitted constraints.

inputs	output
00	0
01	0
10	0
11	1

OR gadget

Blueprint: g <-> (u OR v)

Emitted: (NOT g OR (u OR v)) AND (NOT (u OR v) OR g)

Same shape as AND; only the rhs connective changes.

inputs	output
00	0
01	1
10	1
11	1

NOT gadget

Blueprint: g <-> NOT u

Emitted: (NOT g OR NOT u) AND (u OR g)

Unary form uses one input and the same encoding style.

inputs	output
0	1
1	0

Variable rolesInputs stay as inputs. Every non-input node gets one helper variable.

Inputs

Input variables x1..x4 are problem variables (same names as Circuit-SAT inputs).

Helpers

Helper variables n1, g1, g2, g3, g4, and z are the circuit gate outputs.

Formal reduction sketch

For each gate g:

\text{emit}(g) = (\neg g \lor \text{rhs}) \land (\neg \text{rhs} \lor g),

where rhs is the gate’s local AND, OR, or NOT expression.

The reduced formula is valid in that order because the source circuit is acyclic, so every gate input has already been defined by a source input or earlier gate.

The reduced formula is:

\Phi_C = z \land \bigwedge_{g \in Gates(C)} \text{emit}(g).

Formal constructionThe emitted constraints are real SAT clauses and use AND/OR/NOT only.

Blueprint

Φ_C = z ∧ (∧_{g in Gates(C)} emit(g)), where emit uses only AND/OR/NOT.

Emit (actual)

emit(n1) = ((NOT n1 OR NOT x2)) AND ((NOT (NOT x2) OR n1))

emit(g1) = ((NOT g1 OR (x1 AND n1))) AND ((NOT ((x1 AND n1)) OR g1))

emit(g2) = ((NOT g2 OR (x3 OR x4))) AND ((NOT ((x3 OR x4)) OR g2))

emit(g3) = ((NOT g3 OR (g1 AND g2))) AND ((NOT ((g1 AND g2)) OR g3))

emit(g4) = ((NOT g4 OR (x2 AND x4))) AND ((NOT ((x2 AND x4)) OR g4))

emit(z) = ((NOT z OR (g3 OR g4))) AND ((NOT ((g3 OR g4)) OR z))

append final z

The important point is that Φ_C itself uses only AND, OR, and NOT constraints.

Assignment extension and projection

The reduction outputs a different assignment vocabulary than Circuit-SAT: helper names are added for non-input nodes, and backward reasoning will project back.

Assignment extension and projectionExtend x1..x4 to all helper variables. Restriction keeps only inputs.

1010

input row: x1=1, x2=0, x3=1, x4=0

extended row: x1=1, x2=0, x3=1, x4=0, n1=1, g1=1, g2=1, g3=1, g4=0, z=1

restricted row: x1=1, x2=0, x3=1, x4=0

0101

input row: x1=0, x2=1, x3=0, x4=1

extended row: x1=0, x2=1, x3=0, x4=1, n1=0, g1=0, g2=1, g3=0, g4=1, z=1

restricted row: x1=0, x2=1, x3=0, x4=1

Correctness direction 1: Circuit-SAT → SAT

If a circuit assignment a makes C(a)=1, extend it with all gate helper values. Every local gate constraint is satisfied by that extension, and z=1 is added: so Φ_C is satisfiable under the extended assignment.

Correctness direction 2: SAT → Circuit-SAT

If a formula assignment b satisfies Φ_C, each emitted gate constraint forces every helper to match the corresponding gate output. Reading only b|inputs| gives an input row where z=1, so C(b|inputs|)=1.

That is why both directions are checked in one reduction proof.

Correctness directionsBoth directions are required for equivalence.

Forward (C(a)=1 => Φ_C(â)=1)

1010: C(a)=1 -> Φ_C(â)=1

Backward (Φ_C(b)=1 => C(b|inputs|)=1)

b=1010: Φ_C(b)=1 => C(b|inputs|)=1

Forward witnesses Assignments with C(a)=1 extend to satisfy Φ_C(â).

assignment	C(a)	conjunction without z	final Φ_C(â)
1010	1	1	1
0101	1	1	1

Backward reconstruction Start from a satisfying formula assignment b, restrict it to b|inputs|, then rebuild gate outputs in topological order.

Satisfying witness b = 1010

inputs in b|inputs|: x1=1, x2=0, x3=1, x4=0

extended helper values: x1=1, x2=0, x3=1, x4=0, n1=1, g1=1, g2=1, g3=1, g4=0, z=1

restricted row b|inputs|: x1=1, x2=0, x3=1, x4=0

Satisfying witness b = 0101

inputs in b|inputs|: x1=0, x2=1, x3=0, x4=1

extended helper values: x1=0, x2=1, x3=0, x4=1, n1=0, g1=0, g2=1, g3=0, g4=1, z=1

restricted row b|inputs|: x1=0, x2=1, x3=0, x4=1

Cheating assignment check

If a formula assignment is inconsistent on helpers, the local clauses reject it.

Cheating witness on base inputs 0000:

x1=0, x2=0, x3=0, x4=0, n1=1, g1=1, g2=0, g3=0, g4=0, z=0

NOT g1 OR (x1 AND n1) is false because x1=0 and n1=1 but g1=1.

Dedicated output assertion contrast

Local consistency can be true with z=0; this would be incorrectly accepted without the final AND z.

Dedicated AND z contrastLocal consistency can be true while z=0. AND z is the acceptance filter.

assignment	gate constraints	z	Φ_C	note
0000	1	0	0	Consistency-only assignment that would satisfy all emitted gates but must be rejected by AND z.

This is exactly the AND z contrast: it enforces acceptance, not just consistency.

Master reduction trace over the fixture

Use this master demo to watch gate emission, emitted-prefix growth, and the final check.

Master reduction trace

The reduction evaluates one fixed assignment and emits one constraint per gate in topological order.

emitted constraints so far

Current step

emit n1: n1 <-> (NOT x2) -> ((NOT n1 OR NOT x2)) AND ((NOT (NOT x2) OR n1))

gate value check = 1

Input values must be valid and then every step uses stored predecessors.

Assignment view

inputs x1=1, x2=0, x3=1, x4=0

helpers n1=1

emitted prefix

((NOT n1 OR NOT x2)) AND ((NOT (NOT x2) OR n1))

1 / 7

Blueprint (local)

n1 <-> (NOT x2)

→

Emitted formula so far

((NOT n1 OR NOT x2)) AND ((NOT (NOT x2) OR n1))

Trace sequence
step	work	emitted
1	emit n1	((NOT n1 OR NOT x2)) AND ((NOT (NOT x2) OR n1))
2	emit g1	((NOT g1 OR (x1 AND n1))) AND ((NOT ((x1 AND n1)) OR g1))
3	emit g2	((NOT g2 OR (x3 OR x4))) AND ((NOT ((x3 OR x4)) OR g2))
4	emit g3	((NOT g3 OR (g1 AND g2))) AND ((NOT ((g1 AND g2)) OR g3))
5	emit g4	((NOT g4 OR (x2 AND x4))) AND ((NOT ((x2 AND x4)) OR g4))
6	emit z	((NOT z OR (g3 OR g4))) AND ((NOT ((g3 OR g4)) OR z))
7	assert-output	z

Implementation and invariant

Implementation emits one gadget per gate in topological order, then the final z.

Builder tableOne emitted clause pair per gate, in topological order.

step	gate/helper	blueprint	emitted
1	n1	`n1 <-> (NOT x2)`	`((NOT n1 OR NOT x2)) AND ((NOT (NOT x2) OR n1))`
2	g1	`g1 <-> (x1 AND n1)`	`((NOT g1 OR (x1 AND n1))) AND ((NOT ((x1 AND n1)) OR g1))`
3	g2	`g2 <-> (x3 OR x4)`	`((NOT g2 OR (x3 OR x4))) AND ((NOT ((x3 OR x4)) OR g2))`
4	g3	`g3 <-> (g1 AND g2)`	`((NOT g3 OR (g1 AND g2))) AND ((NOT ((g1 AND g2)) OR g3))`
5	g4	`g4 <-> (x2 AND x4)`	`((NOT g4 OR (x2 AND x4))) AND ((NOT ((x2 AND x4)) OR g4))`
6	z	`z <-> (g3 OR g4)`	`((NOT z OR (g3 OR g4))) AND ((NOT ((g3 OR g4)) OR z))`

Consistency railEach helper is constrained by already-known earlier values.

n1n1 is set from already-known earlier values: x2.

g1g1 is set from already-known earlier values: x1, n1.

g2g2 is set from already-known earlier values: x3, x4.

g3g3 is set from already-known earlier values: g1, g2.

g4g4 is set from already-known earlier values: x2, x4.

zz is set from already-known earlier values: g3, g4.

This is deterministic and linear in gate count.

Complexity

Let |C| count the circuit’s nodes and wiring constants in the fixed encoding. Each non-input node adds one helper variable and one constant-size gadget. One final output clause (z) is added.

Size stackEach of 6 non-input nodes contributes one helper variable and one constant-size gadget; plus final z, so |Φ_C| = O(|C|).

kind	count
Inputs	4
Helper vars	6
Gate constraints	6
Final output assertion	1

So |Φ_C| = O(|C|): one emitted constraint per gate plus one assertion. This linear claim uses fixed fan-in gadgets (AND/OR with two inputs, NOT with one), so each emitted gate encoding stays constant-size.

Common confusions and checks

Common confusions

Keep shorthand, order, and helper roles explicit.

It looks simpler to write `g <-> expr` everywhere, so we can keep that as the output instance.

Repair: No. `<->` is readable shorthand for local comparison. Accumulated SAT output must only use AND/OR/NOT.

If each gate variable matches its local rule, then satisfiability is preserved without extra clauses.

Emit constraints in any order; topological input order is only a coding detail.

Helper gate variables are not needed; only x1..x4 should appear in the formula.

Connections

sat supplies the target language; polynomial-time-reductions supplies the proof pattern; circuit-sat supplies the shared source fixture.

Local graph contextThis bridge is now a concrete source->target reduction between already-known nodes.

polynomial-time-reductions

answer-preserving translators

→

circuit-sat

source SAT instance

→

sat

target language

→

circuit-sat-to-sat

this node

Exercises

Practice the reduction

Classify fixtures and malformed handling by reduction semantics.

If circuit assignment 1010 is satisfying, what should the reduced SAT instance do on the same extension?

Choose an answer to check this item.

For 0000, gate constraints are true. What does final conjunction require?

Choose an answer to check this item.

In the backward direction, a satisfying formula assignment is first restricted to inputs. What is kept?

Choose an answer to check this item.

Which behavior is correct for assignment `101`?

Choose an answer to check this item.

Which rows from the shared fixture witness the reduction as preserving Yes/No answers?
Why is 0000 accepted by all gate constraints but rejected by Φ_C?
Why can’t <-> be the emitted final formula language for SAT?
What are inputs, and what are helper variables?

Graph connections : Circuit-SAT to SAT