Forbidden-pattern compilation from Boolean CSPs to CNF

Every Boolean constraint (R, vs) : Constraint Rel V of scope length r = vs.length ≤ k has at most 2 ^ r ≤ 2 ^ k forbidden local assignments w ∈ BitString.enumList r with sem R w = false. Emitting one width-r clause Constraint.forbidClause vs w per forbidden assignment translates a Boolean CSP instance F : CSP Rel V into an equivalent k-CNF formula F.toCNF sem on a subset of the same variables, with no auxiliary variables and therefore multiplicative factor 1 on satisfying assignments:

• (F.toCNF sem).eval σ = F.eval sem σ for every assignment σ : V → Bool;
• (F.toCNF sem).modelCountOn S = F.modelCountOn sem S for every declared variable set S;
• (F.toCNF sem).length ≤ 2 ^ k * F.length and every generated clause has width ≤ k.

Main definitions

• Cslib.Logic.PL.Constraint.forbidClause: the clause forbidding a local bit pattern on a scope.
• Cslib.Logic.PL.Constraint.toCNF, Cslib.Logic.PL.Constraint.toCNFBounded: compile a Boolean constraint to CNF by forbidding falsifying patterns.
• Cslib.Logic.PL.CSP.toCNF, Cslib.Logic.PL.CSP.toCNFBounded: compile a Boolean CSP instance to CNF.

Main results

• Cslib.Logic.PL.Constraint.eval_forbidClause, Cslib.Logic.PL.Constraint.eval_toCNF, Cslib.Logic.PL.CSP.eval_toCNF: exact evaluation equivalence of the compiled CNF formula.
• Cslib.Logic.PL.CSP.satisfiable_toCNF, Cslib.Logic.PL.CSP.modelCountOn_toCNF: satisfiability and declared-variable model counts are preserved with multiplicity 1.
• Cslib.Logic.PL.CSP.length_clause_mem_toCNFBounded, Cslib.Logic.PL.CSP.validDeclaredInput_toCNFBounded: clause-width and declared-variable bounds.

References

• OpenAI, The Exponential Time Hypothesis is False, Appendix C (p. 52).

def Cslib.Logic.PL.Constraint.forbidClause {V : Type u_2} (vs : List V) (w : List Bool) : Clause V

The clause on scope vs forbidding the local bit pattern w by negating each bit of w.

@[simp]

theorem Cslib.Logic.PL.Constraint.forbidClause_cons {V : Type u_2} (v : V) (vs : List V) (b : Bool) (w : List Bool) : forbidClause (v :: vs) (b :: w) = (v, !b) :: forbidClause vs w

Consing a variable and a bit prepends the negated literal to forbidClause.

@[simp]

theorem Cslib.Logic.PL.Constraint.length_forbidClause {V : Type u_2} (vs : List V) (w : List Bool) : List.length (forbidClause vs w) = min vs.length w.length

The length of forbidClause vs w is min vs.length w.length.

theorem Cslib.Logic.PL.Constraint.length_forbidClause_le {V : Type u_2} (vs : List V) (w : List Bool) : List.length (forbidClause vs w) ≤ vs.length

forbidClause vs w has at most vs.length literals.

theorem Cslib.Logic.PL.Constraint.mem_vars_forbidClause {V : Type u_2} {vs : List V} {w : List Bool} {l : Literal V} (hl : l ∈ forbidClause vs w) : l.1 ∈ vs

Every variable in forbidClause vs w belongs to vs.

theorem Cslib.Logic.PL.Constraint.relabel_forbidClause {V : Type u_2} {W : Type u_3} (f : V → W) (vs : List V) (w : List Bool) : Clause.relabel f (forbidClause vs w) = forbidClause (List.map f vs) w

Relabeling forbidClause vs w maps f over the scope vs.

theorem Cslib.Logic.PL.Constraint.eval_forbidClause {V : Type u_2} (vs : List V) {w : List Bool} (hw : w.length = vs.length) (σ : V → Bool) : Clause.eval σ (forbidClause vs w) = !List.map σ vs == w

forbidClause vs w evaluates to false under σ if and only if vs.map σ = w (even when vs contains repeated variables).

def Cslib.Logic.PL.Constraint.toCNF {Rel : Type u_1} {V : Type u_2} (sem : Rel → List Bool → Bool) (c : Constraint Rel V) : CNF V

Compile a Boolean constraint c = (R, vs) to a CNF formula by emitting forbidClause vs w for every forbidden local assignment w ∈ BitString.enumList vs.length with sem R w = false.

def Cslib.Logic.PL.Constraint.toCNFBounded {Rel : Type u_1} {V : Type u_2} (k : ℕ) (sem : Rel → List Bool → Bool) (c : Constraint Rel V) : CNF V

Width-guarded compilation: emits toCNF sem c when c.2.length ≤ k and [] otherwise.

theorem Cslib.Logic.PL.Constraint.toCNFBounded_eq_toCNF {Rel : Type u_1} {V : Type u_2} {k : ℕ} {sem : Rel → List Bool → Bool} {c : Constraint Rel V} (hc : c.2.length ≤ k) : toCNFBounded k sem c = toCNF sem c

When c.2.length ≤ k, toCNFBounded k sem c agrees with toCNF sem c.

theorem Cslib.Logic.PL.Constraint.length_clause_mem_toCNF {Rel : Type u_1} {V : Type u_2} {sem : Rel → List Bool → Bool} {c : Constraint Rel V} {cl : Clause V} (hcl : cl ∈ toCNF sem c) : List.length cl ≤ c.2.length

Every clause in c.toCNF sem has length at most c.2.length.

theorem Cslib.Logic.PL.Constraint.length_clause_mem_toCNFBounded {Rel : Type u_1} {V : Type u_2} {k : ℕ} {sem : Rel → List Bool → Bool} {c : Constraint Rel V} {cl : Clause V} (hcl : cl ∈ toCNFBounded k sem c) : List.length cl ≤ k

Every clause in c.toCNFBounded k sem has length at most k.

theorem Cslib.Logic.PL.Constraint.length_toCNF_le {Rel : Type u_1} {V : Type u_2} (sem : Rel → List Bool → Bool) (c : Constraint Rel V) : List.length (toCNF sem c) ≤ 2 ^ c.2.length

c.toCNF sem contains at most 2 ^ c.2.length clauses.

theorem Cslib.Logic.PL.Constraint.mem_vars_toCNF {Rel : Type u_1} {V : Type u_2} {sem : Rel → List Bool → Bool} {c : Constraint Rel V} {v : V} (hv : v ∈ (toCNF sem c).vars) : v ∈ c.2

Every variable occurring in c.toCNF sem belongs to the constraint scope c.2.

theorem Cslib.Logic.PL.Constraint.mem_vars_toCNFBounded {Rel : Type u_1} {V : Type u_2} {k : ℕ} {sem : Rel → List Bool → Bool} {c : Constraint Rel V} {v : V} (hv : v ∈ (toCNFBounded k sem c).vars) : v ∈ c.2

Every variable occurring in c.toCNFBounded k sem belongs to the constraint scope c.2.

theorem Cslib.Logic.PL.Constraint.relabel_toCNF {Rel : Type u_1} {V : Type u_2} {W : Type u_3} (sem : Rel → List Bool → Bool) (f : V → W) (c : Constraint Rel V) : CNF.relabel f (toCNF sem c) = toCNF sem (relabel f c)

Relabeling commutes with Constraint.toCNF.

theorem Cslib.Logic.PL.Constraint.relabel_toCNFBounded {Rel : Type u_1} {V : Type u_2} {W : Type u_3} (k : ℕ) (sem : Rel → List Bool → Bool) (f : V → W) (c : Constraint Rel V) : CNF.relabel f (toCNFBounded k sem c) = toCNFBounded k sem (relabel f c)

Relabeling commutes with Constraint.toCNFBounded.

@[simp]

theorem Cslib.Logic.PL.Constraint.eval_toCNF {Rel : Type u_1} {V : Type u_2} (sem : Rel → List Bool → Bool) (c : Constraint Rel V) (σ : V → Bool) : CNF.eval σ (toCNF sem c) = eval sem σ c

The forbidden-assignment CNF compilation of a constraint has the exact same truth value under every assignment σ : V → Bool as the constraint itself.

def Cslib.Logic.PL.CSP.toCNF {Rel : Type u_1} {V : Type u_2} (sem : Rel → List Bool → Bool) (F : CSP Rel V) : CNF V

Compile a Boolean CSP instance F to a CNF formula by concatenating the forbidden-assignment clauses of each constraint.

def Cslib.Logic.PL.CSP.toCNFBounded {Rel : Type u_1} {V : Type u_2} (k : ℕ) (sem : Rel → List Bool → Bool) (F : CSP Rel V) : CNF V

Width-guarded compilation of F to a k-CNF formula.

theorem Cslib.Logic.PL.CSP.toCNFBounded_eq_toCNF {Rel : Type u_1} {V : Type u_2} {k : ℕ} {sem : Rel → List Bool → Bool} {F : CSP Rel V} (hF : ∀ c ∈ F, c.2.length ≤ k) : toCNFBounded k sem F = toCNF sem F

When all constraint scopes in F have length ≤ k, F.toCNFBounded k sem = F.toCNF sem.

theorem Cslib.Logic.PL.CSP.length_clause_mem_toCNFBounded {Rel : Type u_1} {V : Type u_2} {k : ℕ} {sem : Rel → List Bool → Bool} {F : CSP Rel V} {cl : Clause V} (hcl : cl ∈ toCNFBounded k sem F) : List.length cl ≤ k

Every clause in F.toCNFBounded k sem has length at most k.

theorem Cslib.Logic.PL.CSP.length_clause_mem_toCNF {Rel : Type u_1} {V : Type u_2} {k : ℕ} {sem : Rel → List Bool → Bool} {F : CSP Rel V} (hF : ∀ c ∈ F, c.2.length ≤ k) {cl : Clause V} (hcl : cl ∈ toCNF sem F) : List.length cl ≤ k

When all constraint scopes in F have length ≤ k, every clause in F.toCNF sem has length at most k.

theorem Cslib.Logic.PL.CSP.length_toCNF_le {Rel : Type u_1} {V : Type u_2} {k : ℕ} (sem : Rel → List Bool → Bool) {F : CSP Rel V} (hF : ∀ c ∈ F, c.2.length ≤ k) : List.length (toCNF sem F) ≤ 2 ^ k * List.length F

When all constraint scopes in F have length ≤ k, F.toCNF sem has at most 2 ^ k * F.length clauses.

theorem Cslib.Logic.PL.CSP.mem_vars_toCNF {Rel : Type u_1} {V : Type u_2} {sem : Rel → List Bool → Bool} {F : CSP Rel V} {v : V} (hv : v ∈ (toCNF sem F).vars) : v ∈ F.vars

Every variable occurring in F.toCNF sem occurs in F.vars.

theorem Cslib.Logic.PL.CSP.mem_vars_toCNFBounded {Rel : Type u_1} {V : Type u_2} {k : ℕ} {sem : Rel → List Bool → Bool} {F : CSP Rel V} {v : V} (hv : v ∈ (toCNFBounded k sem F).vars) : v ∈ F.vars

Every variable occurring in F.toCNFBounded k sem occurs in F.vars.

theorem Cslib.Logic.PL.CSP.relabel_toCNF {Rel : Type u_1} {V : Type u_2} {W : Type u_3} (sem : Rel → List Bool → Bool) (f : V → W) (F : CSP Rel V) : CNF.relabel f (toCNF sem F) = toCNF sem (relabel f F)

Relabeling commutes with CSP.toCNF.

theorem Cslib.Logic.PL.CSP.relabel_toCNFBounded {Rel : Type u_1} {V : Type u_2} {W : Type u_3} (k : ℕ) (sem : Rel → List Bool → Bool) (f : V → W) (F : CSP Rel V) : CNF.relabel f (toCNFBounded k sem F) = toCNFBounded k sem (relabel f F)

Relabeling commutes with CSP.toCNFBounded.

@[simp]

theorem Cslib.Logic.PL.CSP.eval_toCNF {Rel : Type u_1} {V : Type u_2} (sem : Rel → List Bool → Bool) (F : CSP Rel V) (σ : V → Bool) : CNF.eval σ (toCNF sem F) = eval sem σ F

The compiled CNF formula F.toCNF sem evaluates identically to F under every assignment.

@[simp]

theorem Cslib.Logic.PL.CSP.satisfiable_toCNF {Rel : Type u_1} {V : Type u_2} (sem : Rel → List Bool → Bool) (F : CSP Rel V) : (toCNF sem F).Satisfiable ↔ Satisfiable sem F

F.toCNF sem is satisfiable if and only if F is satisfiable under sem.

@[simp]

theorem Cslib.Logic.PL.CSP.modelCountOn_toCNF {Rel : Type u_1} {V : Type u_2} [DecidableEq V] (sem : Rel → List Bool → Bool) (F : CSP Rel V) (declared : Finset V) : (toCNF sem F).modelCountOn declared = modelCountOn sem F declared

Forbidden-assignment CNF compilation preserves declared-variable model counts on every finite variable set declared with multiplicity 1 (no auxiliary variables).

theorem Cslib.Logic.PL.CSP.validDeclaredInput_toCNFBounded {Rel : Type u_1} {k N : ℕ} (sem : Rel → List Bool → Bool) {F : CSP Rel ℕ} (hv : validDeclaredCSP k N F = true) : CNF.validDeclaredInput k N (toCNFBounded k sem F) = true

If F passes validDeclaredCSP k N, then F.toCNFBounded k sem passes CNF.validDeclaredInput k N.