Circuit satisfiability

CircuitSAT is the set of De Morgan circuits with one output that output true on some input Arora and Barak, Section 6.1. Circuits are encoded by Cslib.Circuits.Boolean.encCircuit: the number n of inputs in unary, then the gates in program order with wire numbers in binary, then the output wire. Since n is written in unary, the encoding is at least n bits long, and an assignment to the inputs fits in a certificate as long as the encoding.

CircuitSAT is NP-complete (Cslib.Complexity.CircuitSAT_npComplete). It is in NP: the verifier evaluates the circuit on the first n bits of the certificate. It is NP-hard because SAT reduces to it (Cslib.Complexity.SAT.polyTimeReducible_CircuitSAT) and SAT is NP-complete by the Cook–Levin theorem. The circuit of a formula (Cslib.Complexity.SAT.toCircuit) has one input for each literal occurrence; a variable is read at the input of its first occurrence, as for the certificates of SAT.verifier. Its gates come in blocks of three, one block for each literal and one for the end of each clause, which keep the disjunction of the current clause and the conjunction of the finished clauses at fixed offsets from the end.

Main definitions

• Cslib.Complexity.SignatureCircuitSAT: the satisfiable single-output circuits over an arbitrary Boolean signature and interpretation.
• Cslib.Complexity.CircuitSAT: the satisfiable De Morgan circuits with one output.
• Cslib.Complexity.CircuitSAT.verifier: evaluation on the first bits of a certificate.
• Cslib.Complexity.SAT.toCircuit: the circuit of a formula in conjunctive normal form.

Main results

• Cslib.Complexity.signatureCircuitSAT_boolean: specializing SignatureCircuitSAT to the De Morgan basis recovers CircuitSAT.
• Cslib.Complexity.CircuitSAT.mem_NP: circuit satisfiability is in NP.
• Cslib.Complexity.SAT.toCircuit_mem_CircuitSAT_iff: the circuit of a formula is satisfiable exactly when the formula is.
• Cslib.Complexity.SAT.polyTimeReducible_CircuitSAT: SAT reduces to CircuitSAT in polynomial time.
• Cslib.Complexity.CircuitSAT_npHard, Cslib.Complexity.CircuitSAT_npComplete: circuit satisfiability is NP-hard and NP-complete.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 6.1

def Cslib.Complexity.SignatureCircuitSAT {σ : Circuits.Signature} (I : Circuits.Interpretation σ Bool) : Set ((n : ℕ) × Circuits.Circuit σ n 1)

Circuit satisfiability over an arbitrary Boolean signature: the single-output circuits over σ that output true under I on some input.

theorem Cslib.Complexity.mem_SignatureCircuitSAT {σ : Circuits.Signature} {I : Circuits.Interpretation σ Bool} {c : (n : ℕ) × Circuits.Circuit σ n 1} : c ∈ SignatureCircuitSAT I ↔ ∃ (x : BitString c.fst), c.snd.eval I x 0 = true

Membership in SignatureCircuitSAT I.

def Cslib.Complexity.CircuitSAT : Set ((n : ℕ) × Circuits.Circuit Circuits.Boolean.signature n 1)

Circuit satisfiability: the De Morgan circuits with one output that output true on some input Arora and Barak, Section 6.1.

@[simp]

theorem Cslib.Complexity.signatureCircuitSAT_boolean : SignatureCircuitSAT Circuits.Boolean.interpretation = CircuitSAT

Specializing SignatureCircuitSAT to the De Morgan basis recovers CircuitSAT.

theorem Cslib.Complexity.mem_CircuitSAT {c : (n : ℕ) × Circuits.Circuit Circuits.Boolean.signature n 1} : c ∈ CircuitSAT ↔ ∃ (x : BitString c.fst), c.snd.eval Circuits.Boolean.interpretation x 0 = true

Membership in NP

def Cslib.Complexity.CircuitSAT.verifier (p : ((n : ℕ) × Circuits.Circuit Circuits.Boolean.signature n 1) × List Bool) : Bool

The verifier for CircuitSAT: evaluate the circuit on the first bits of the certificate, reading missing bits as false.

theorem Cslib.Complexity.CircuitSAT.isVerifier : IsVerifier (Circuits.Boolean.encCircuit 1) Polynomial.X verifier CircuitSAT

CircuitSAT.verifier verifies CircuitSAT with certificates as long as the encoded circuit.

theorem Cslib.Complexity.CircuitSAT.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair (Circuits.Boolean.encCircuit 1) Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The CircuitSAT verifier is polynomial-time, on certificates of arbitrary length.

theorem Cslib.Complexity.CircuitSAT.mem_NP : CircuitSAT ∈ NP (Circuits.Boolean.encCircuit 1)

Circuit satisfiability is in NP, with certificates as long as the encoded circuit.

The circuit of a formula

def Cslib.Complexity.SAT.circuitSteps (φ : Logic.PL.CNF ℕ) : List (Logic.PL.Literal ℕ × Bool)

The instructions building the circuit of a formula: each literal of each clause, flagged false, and after each clause an end marker flagged true (with a placeholder literal).

def Cslib.Complexity.SAT.circuitBlock (p i : ℕ) (b e : Bool) : List (Circuits.Boolean.Op × List ℕ)

The three gates of one instruction, when the three gates before it are the wires p, p + 1 and p + 2, the last two holding the disjunction of the current clause so far and the conjunction of the finished clauses. For the literal (v, b) read at input i, the gates compute the literal, add it to the clause and copy the conjunction. At the end of a clause they compute the conjunction with the clause, restart the clause at false and copy the conjunction.

def Cslib.Complexity.SAT.circuitGates (φ : Logic.PL.CNF ℕ) : List (Circuits.Boolean.Op × List ℕ)

The gates of the circuit of a formula with n literal occurrences: three constant gates starting the clause at false and the conjunction at true, then the block of each instruction. The block of instruction t follows the gates 3 t, 3 t + 1, 3 t + 2, which are the wires n + 3 t, n + 3 t + 1 and n + 3 t + 2.

def Cslib.Complexity.SAT.circuitCode (φ : Logic.PL.CNF ℕ) : List (Circuits.Boolean.Op × List ℕ) × List ℕ

The code of the circuit of a formula: its gates and, as output, the last conjunction.

theorem Cslib.Complexity.SAT.isSome_ofCode_circuitCode (φ : Logic.PL.CNF ℕ) : (Circuits.Circuit.ofCode φ.vars.length 1 (circuitCode φ)).isSome = true

The circuit code of a formula is the code of a circuit with one output.

def Cslib.Complexity.SAT.toCircuit (φ : Logic.PL.CNF ℕ) : (n : ℕ) × Circuits.Circuit Circuits.Boolean.signature n 1

The circuit of a formula: one input for each literal occurrence, and the gates of circuitCode.

Correctness of the circuit of a formula

theorem Cslib.Complexity.SAT.eval_toCircuit (φ : Logic.PL.CNF ℕ) (x : BitString (toCircuit φ).fst) : (toCircuit φ).snd.eval Circuits.Boolean.interpretation x 0 = Logic.PL.CNF.eval (assignment φ (List.ofFn x)) φ

The circuit of a formula evaluates it: on input x, it outputs the value of the formula under the assignment giving each variable the input bit at its first occurrence (SAT.assignment).

theorem Cslib.Complexity.SAT.toCircuit_mem_CircuitSAT_iff (φ : Logic.PL.CNF ℕ) : toCircuit φ ∈ CircuitSAT ↔ φ ∈ SAT

The circuit of a formula is satisfiable exactly when the formula is.

The reduction is polynomial-time

theorem Cslib.Complexity.SAT.polyTimeReducible_CircuitSAT : PolyTimeReducible encCNF (Circuits.Boolean.encCircuit 1) SAT CircuitSAT

SAT reduces to CircuitSAT in polynomial time.

theorem Cslib.Complexity.CircuitSAT_npHard : NPHard (Circuits.Boolean.encCircuit 1) CircuitSAT

Circuit satisfiability is NP-hard.

theorem Cslib.Complexity.CircuitSAT_npComplete : NPComplete (Circuits.Boolean.encCircuit 1) CircuitSAT

Circuit satisfiability is NP-complete, for the binary encoding of circuits encCircuit 1 Arora and Barak, Section 6.1.