Numbered assignments

Exhaustive search over the assignments of the n distinct variables of a formula enumerates the numbers i < 2 ^ n. Cslib.Logic.PL.bitsAssignment vs i gives the variable at position j of the list vs the binary digit j of i. Every assignment of the variables of a duplicate-free list vs is numbered by some i < 2 ^ |vs| (Cslib.Logic.PL.exists_lt_two_pow_bitsAssignment_eq), so a formula whose variables are listed by vs is satisfiable exactly when one of the numbered assignments satisfies it (Cslib.Logic.PL.CNF.satisfiable_iff_exists_bitsAssignment). The distinct variables of a formula are listed by Cslib.Complexity.ThreeSAT.distinctVars, of length Cslib.Logic.PL.CNF.numVars (Cslib.Complexity.ThreeSAT.length_distinctVars). Evaluating a formula under a numbered assignment is polynomial-time (Cslib.Complexity.computableTidilyInPolyTime_eval_bitsAssignment).

Main definitions

• Cslib.Logic.PL.bitsAssignment: the assignment numbered by i.

Main results

• Cslib.Logic.PL.CNF.satisfiable_iff_exists_bitsAssignment: satisfiability is a search over 2 ^ |vs| numbered assignments.
• Cslib.Complexity.ThreeSAT.length_distinctVars: a formula has numVars distinct variables.
• Cslib.Complexity.computableTidilyInPolyTime_eval_bitsAssignment: evaluation under a numbered assignment is polynomial-time.

References

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

def Cslib.Logic.PL.bitsAssignment {V : Type u_1} [DecidableEq V] (vs : List V) (i : ℕ) (v : V) : Bool

The assignment numbered by i on the list of variables vs: the variable at position j of vs takes the binary digit j of i.

theorem Cslib.Logic.PL.exists_lt_two_pow_bitsAssignment_eq {V : Type u_1} [DecidableEq V] {vs : List V} (σ : V → Bool) : ∃ i < 2 ^ vs.length, ∀ v ∈ vs, bitsAssignment vs i v = σ v

Every assignment is numbered. The assignments of the variables of a duplicate-free list vs are the numbered assignments bitsAssignment vs i for i < 2 ^ |vs|.

theorem Cslib.Logic.PL.CNF.satisfiable_iff_exists_bitsAssignment {V : Type u_1} [DecidableEq V] {φ : CNF V} {vs : List V} (hφ : ∀ v ∈ φ.vars, v ∈ vs) : φ.Satisfiable ↔ ∃ i < 2 ^ vs.length, eval (bitsAssignment vs i) φ = true

Satisfiability by exhaustive search. A formula whose variables are all in the list vs is satisfiable exactly when it is satisfied by an assignment numbered by some i < 2 ^ |vs|.

theorem Cslib.Logic.PL.bitsAssignment_eq_getD {V : Type u_1} [DecidableEq V] (vs : List V) (i : ℕ) (v : V) : bitsAssignment vs i v = i.bits.getD (List.idxOf v vs) false

The distinct variables

theorem Cslib.Complexity.ThreeSAT.mem_distinctVars {φ : Logic.PL.CNF ℕ} {v : ℕ} : v ∈ distinctVars φ ↔ v ∈ φ.vars

theorem Cslib.Complexity.ThreeSAT.length_distinctVars (φ : Logic.PL.CNF ℕ) : (distinctVars φ).length = φ.numVars

A formula has numVars distinct variables.

Polynomial time

theorem Cslib.Complexity.computableTidilyInPolyTime_eval_bitsAssignment : Turing.MultiTapeTM.ComputableTidilyInPolyTime (fun (p : (Logic.PL.CNF ℕ × List ℕ) × ℕ) => Logic.PL.CNF.eval (Logic.PL.bitsAssignment p.1.2 p.2) p.1.1) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encCNF (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encNat)) Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

Evaluating a formula under the assignment numbered by i on a list of variables is polynomial-time.