CIRCUIT-SAT poly-reduces to SAT

The reduction of CLRS Lemma 34.6: a boolean circuit is satisfiable iff the boolean formula obtained by asserting the consistency of every gate (and the output) is satisfiable. The construction introduces a variable per wire and one ↔-formula per gate.

Main results:

• Model Formula (variables, constants, not/and/or/iff) with evaluation Formula.eval and satisfiable.

• Model Gate (input, constant, not/and/or) and a circuit as a list of gates, with wire evaluation evalWire and circuitSatisfiable.

• The reduction circuitToFormula, and the correctness theorem circuitSatisfiable_iff_satisfiable_circuitToFormula (Lemma 34.6, the semantic half).

• The prefix-polish list encoding enc/circuitToFormulaList, the decoder decode (with decode_enc), and the languages CIRCUIT_SAT and SAT.

• The reduction TM2 machine Turing.TM2CS.mach, its phase simulation csOutputsFun, the polynomial time bound csTime, and the csComputableInPolyTime instance.

• The assembled circuitSAT_reducible_to_SAT: CIRCUIT_SAT ≤_P SAT (CLRS Lemma 34.6).

Current status: complete and kernel-clean. The semantic equivalence, the list encoding and decoding, the machine program (count/reorder/header/ loop/emitTrue/copyOut phases), the outputsFun phase simulation, the polynomial time bound, and the assembled PolyTimeReducible CIRCUIT_SAT SAT are all in place.

The machine emits each gate's clause in a move-then-restore pattern (counter → scratch → output + counter), with the emit labels setting the carried state via load so the move/restore phases stay uniform.

Design (offset wires so every gate has two predecessors):

• Wire 0 and wire 1 are the circuit's input wires (their value is chosen by the assignment σ).

• Gate i (0-indexed) produces wire i + 2, whose inputs are wires i + 1 and i. So a circuit with n gates has wires 0..n+1, and the output is the last wire n + 1.

• circuitToFormula gates is x_{n+1} ∧ ⋀ᵢ (x_{i+2} ↔ gateExprᵢ), where gateExprᵢ is the value of gate i in terms of wires i+1 and i.

With this offset, every wire referenced by a gate exists, so the equivalence holds for every gate list (no well-formedness side condition).

A boolean formula: variables indexed by Nat, constants, and the standard connectives (including ↔, used by the reduction).

Evaluate a formula under an assignment σ : Nat → Bool of its variables.

A formula is satisfiable when some assignment makes it true.

A boolean circuit gate: an input wire, a constant, or a not/and/or gate. A circuit is a list of gates; gate i produces wire i + 2.

The value of a circuit's gate i expressed as a formula in the two predecessor wires i + 1 and i (the wires feeding gate i).

The value of wire i of a circuit, given an assignment σ to the input wires 0 and 1. Wires 0/1 are the inputs; wire i + 2 is gate i's output (and false when i is past the end of the gate list).

The consistency formula for a gate: the gate's output wire equals the value of its expression in the predecessor wires.

The conjunction of the consistency formulas of all gates, in gate order, tracking the wire index.

The conjunction of the consistency formulas of all gates, in gate order.

A circuit is satisfiable when some assignment to the input wires makes the output wire (the last wire, gates.length + 1) true.

The CIRCUIT-SAT → SAT reduction (CLRS Lemma 34.6). Assert the output wire and the consistency of every gate.

The value of gate i's output wire equals the evaluation of its expression formula under the wire-value assignment.

For a wire that is actually produced by gate i, its value equals the evaluation of the gate's expression formula under the wire-value assignment.

Bool equality reflected as == is true exactly when the values are equal.

The getElem? at the boundary of pre ++ g :: rest is g.

The conjunction of all gate-consistency formulas, from a suffix of the gate list, evaluates to true under the wire-value assignment.

The conjunction of the consistency formulas of all gates evaluates to true under the wire-value assignment.

If the conjunction of gate formulas evaluates to true, then every individual gate's consistency formula evaluates to true.

Under a satisfying assignment of circuitToFormula gates, every wire's value matches the assignment's value for that variable.

Theorem (CIRCUIT-SAT poly-reduces to SAT, semantic half, Lemma 34.6). A circuit is satisfiable iff the formula asserting the output wire and the consistency of every gate is satisfiable.

The output alphabet of the reduction: prefix-polish formula symbols.

Encode a variable as varMark followed by i + 1 endMarks (unary index).

Encode a formula in prefix-polish form.

Encode a gate's expression formula (in terms of the wire index) as a list.

Encode the consistency formula of gate i.

The list of gate-consistency encodings, each prefixed by andMark.

The reduction circuitToFormula at the list-encoding level: the header (andMark, the output variable), each gate's consistency formula in order, and the trailing lit true.

The gate-consistency encoding agrees with enc on gateFormula.

The list of gate-consistency encodings (plus the trailing lit true) agrees with enc on the folded gateFormulasAux.

The list encoding agrees with enc on circuitToFormula.

Decode a unary variable index: after a varMark, i + 1 endMarks encode wire i. This helper consumes the run of endMarks, adding their count to the running index.

Decode the unary variable that starts with a varMark (already consumed).

Decode a single prefix-polish formula, returning it and the unconsumed suffix. The first argument is a budget of remaining connective levels; it only needs to exceed the formula depth and equals the encoding length in decode. Malformed or over-budget input yields the junk formula const false.

Decode a formula from its prefix-polish encoding (junk on malformed input).

A list that does not begin with an endMark, so that a variable's unary index run cannot run into it. The continuation after any formula encoding satisfies this.

The empty continuation is valid.

The continuation after an encoded formula never begins with endMark.

decodeVarIdx on a valid continuation leaves it untouched.

decodeVarIdx consumes j endMarks, raising the index by j (leaving a valid continuation untouched).

decodeVar recovers wire j from its j + 1 endMarks (leaving a valid continuation untouched).

Every formula encoding has length at least one.

decodeAux with a sufficient budget consumes exactly the encoding of a formula, leaving a valid continuation untouched.