Positive exact-one satisfiability

All four positive languages prohibit negated literals. Three bounds clause length by three; ExactThree requires three distinct variables in each clause. The final Three bounds total literal occurrences per variable by three, including repeated positions.

These notions reuse the signed CNF representation and the occurrence-count semantics CNF.evalOne. Certificates use the same first-occurrence assignment as ordinary SAT.

Main definitions

• PositiveOneInThreeSAT, PositiveOneInExactThreeSAT.
• PositiveOneInThreeSATThree, PositiveOneInExactThreeSATThree.
• OneSAT: exact-one satisfiability without syntax restrictions.

Main results

• OneSAT.mem_NP: unrestricted exact-one satisfiability belongs to NP.
• Each positive language has an analogous mem_NP theorem.

References

• Hunt, Marathe, Radhakrishnan and Stearns, Definition 2.9 and Theorem 3.8.

def Cslib.Complexity.OneSAT : Set (Logic.PL.CNF ℕ)

Exact-one satisfiable formulas, without a clause-size or polarity restriction.

def Cslib.Complexity.OneSAT.verifier (x : Logic.PL.CNF ℕ × List Bool) : Bool

Evaluate exact-one clauses under the usual first-occurrence certificate assignment.

theorem Cslib.Complexity.OneSAT.isVerifier : IsVerifier encCNF Polynomial.X verifier OneSAT

The standard SAT certificates also represent every exact-one satisfying assignment.

theorem Cslib.Complexity.OneSAT.computableInPolyTime_clause_count : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CNF ℕ × List Bool) × Logic.PL.Clause ℕ) => List.countP (Logic.PL.Literal.eval (SAT.assignment p.1.1 p.1.2)) p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encBits) (Logic.PL.encClause Turing.MultiTapeTM.encNat)) Turing.MultiTapeTM.encUnary

Count the true literal occurrences of a clause in native polynomial time.

theorem Cslib.Complexity.OneSAT.computableInPolyTime_clause : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : (Logic.PL.CNF ℕ × List Bool) × Logic.PL.Clause ℕ) => Logic.PL.Clause.evalOne (SAT.assignment p.1.1 p.1.2) p.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encBits) (Logic.PL.encClause Turing.MultiTapeTM.encNat)) Turing.MultiTapeTM.encBool

An exact-one clause is verified in polynomial time.

theorem Cslib.Complexity.OneSAT.computableInPolyTime_verifier : Turing.MultiTapeTM.ComputableInPolyTime verifier (Turing.MultiTapeTM.encPair encCNF Turing.MultiTapeTM.encBits) Turing.MultiTapeTM.encBool

The exact-one verifier is polynomial-time for binary formula labels.

theorem Cslib.Complexity.OneSAT.mem_NP : OneSAT ∈ NP encCNF

Exact-one satisfiability belongs to NP.

def Cslib.Complexity.OneSAT.positiveCheck (φ : Logic.PL.CNF ℕ) : Bool

Check that all literal polarities are positive.

theorem Cslib.Complexity.OneSAT.positiveCheck_iff (φ : Logic.PL.CNF ℕ) : positiveCheck φ = true ↔ ∀ c ∈ φ, ∀ l ∈ c, l.2 = true

Positivity means that every occurring literal has polarity true.

def Cslib.Complexity.OneSAT.exactClauseCheck (c : Logic.PL.Clause ℕ) : Bool

Check for three distinct variable positions without any restriction on the input length.

theorem Cslib.Complexity.OneSAT.exactClauseCheck_iff (c : Logic.PL.Clause ℕ) : exactClauseCheck c = true ↔ List.length c = 3 ∧ (List.map Prod.fst c).Nodup

The exact-clause check requires three pairwise distinct variables.

theorem Cslib.Complexity.OneSAT.computableInPolyTime_positiveCheck : Turing.MultiTapeTM.ComputableInPolyTime positiveCheck encCNF Turing.MultiTapeTM.encBool

Positivity is decidable in native polynomial time.

theorem Cslib.Complexity.OneSAT.computableInPolyTime_exactClauseCheck : Turing.MultiTapeTM.ComputableInPolyTime exactClauseCheck (Logic.PL.encClause Turing.MultiTapeTM.encNat) Turing.MultiTapeTM.encBool

Exact length and distinctness of a clause are decidable in native polynomial time.

def Cslib.Complexity.PositiveOneInThreeSAT : Set (Logic.PL.CNF ℕ)

Positive exact-one satisfiability with at most three literals per clause.

def Cslib.Complexity.PositiveOneInExactThreeSAT : Set (Logic.PL.CNF ℕ)

Positive exact-one satisfiability with exactly three distinct variables per clause.

def Cslib.Complexity.PositiveOneInThreeSATThree : Set (Logic.PL.CNF ℕ)

Positive width-three exact-one satisfiability with at most three occurrences per variable.

def Cslib.Complexity.PositiveOneInExactThreeSATThree : Set (Logic.PL.CNF ℕ)

Positive exact-three exact-one satisfiability with at most three occurrences per variable.

def Cslib.Complexity.PositiveOneInThreeSAT.syntaxCheck (φ : Logic.PL.CNF ℕ) : Bool

The positive width-three syntax guard.

theorem Cslib.Complexity.PositiveOneInThreeSAT.syntaxCheck_iff (φ : Logic.PL.CNF ℕ) : syntaxCheck φ = true ↔ (∀ c ∈ φ, List.length c ≤ 3) ∧ OneSAT.positiveCheck φ = true

The syntax guard checks exactly the nonsemantic restrictions.

theorem Cslib.Complexity.PositiveOneInThreeSAT.computableInPolyTime_syntaxCheck : Turing.MultiTapeTM.ComputableInPolyTime syntaxCheck encCNF Turing.MultiTapeTM.encBool

The positive width-three syntax guard is polynomial-time.

theorem Cslib.Complexity.PositiveOneInThreeSAT.mem_iff_syntaxCheck (φ : Logic.PL.CNF ℕ) : φ ∈ PositiveOneInThreeSAT ↔ syntaxCheck φ = true ∧ φ ∈ OneSAT

Membership is the syntax guard together with exact-one satisfiability.

theorem Cslib.Complexity.PositiveOneInThreeSAT.mem_NP : PositiveOneInThreeSAT ∈ NP encCNF

Positive width-three exact-one satisfiability belongs to NP.

def Cslib.Complexity.PositiveOneInExactThreeSAT.syntaxCheck (φ : Logic.PL.CNF ℕ) : Bool

The positive exact-three syntax guard.

theorem Cslib.Complexity.PositiveOneInExactThreeSAT.syntaxCheck_iff (φ : Logic.PL.CNF ℕ) : syntaxCheck φ = true ↔ (∀ c ∈ φ, List.length c = 3 ∧ (List.map Prod.fst c).Nodup) ∧ OneSAT.positiveCheck φ = true

The syntax guard checks three distinct variables and positivity.

theorem Cslib.Complexity.PositiveOneInExactThreeSAT.computableInPolyTime_syntaxCheck : Turing.MultiTapeTM.ComputableInPolyTime syntaxCheck encCNF Turing.MultiTapeTM.encBool

The positive exact-three syntax guard is polynomial-time.

theorem Cslib.Complexity.PositiveOneInExactThreeSAT.mem_iff_syntaxCheck (φ : Logic.PL.CNF ℕ) : φ ∈ PositiveOneInExactThreeSAT ↔ syntaxCheck φ = true ∧ φ ∈ OneSAT

Membership is the syntax guard together with exact-one satisfiability.

theorem Cslib.Complexity.PositiveOneInExactThreeSAT.mem_NP : PositiveOneInExactThreeSAT ∈ NP encCNF

Positive exact-three exact-one satisfiability belongs to NP.

def Cslib.Complexity.PositiveOneInThreeSATThree.syntaxCheck (φ : Logic.PL.CNF ℕ) : Bool

Check positivity, width three, and at most three occurrences per variable.

theorem Cslib.Complexity.PositiveOneInThreeSATThree.computableInPolyTime_syntaxCheck : Turing.MultiTapeTM.ComputableInPolyTime syntaxCheck encCNF Turing.MultiTapeTM.encBool

The bounded positive syntax guard is polynomial-time.

theorem Cslib.Complexity.PositiveOneInThreeSATThree.syntaxCheck_iff (φ : Logic.PL.CNF ℕ) : syntaxCheck φ = true ↔ (∀ c ∈ φ, List.length c ≤ 3) ∧ OneSAT.positiveCheck φ = true ∧ ∀ (v : ℕ), List.count v φ.vars ≤ 3

The bounded positive syntax guard checks exactly the syntactic restrictions.

theorem Cslib.Complexity.PositiveOneInThreeSATThree.mem_iff_syntaxCheck (φ : Logic.PL.CNF ℕ) : φ ∈ PositiveOneInThreeSATThree ↔ syntaxCheck φ = true ∧ φ ∈ OneSAT

Membership is the syntax guard together with exact-one satisfiability.

theorem Cslib.Complexity.PositiveOneInThreeSATThree.mem_NP : PositiveOneInThreeSATThree ∈ NP encCNF

Positive width-three exact-one satisfiability with occurrence bound three belongs to NP.

def Cslib.Complexity.PositiveOneInExactThreeSATThree.syntaxCheck (φ : Logic.PL.CNF ℕ) : Bool

Check positive exact-three clauses and the occurrence bound three.

theorem Cslib.Complexity.PositiveOneInExactThreeSATThree.computableInPolyTime_syntaxCheck : Turing.MultiTapeTM.ComputableInPolyTime syntaxCheck encCNF Turing.MultiTapeTM.encBool

The bounded positive exact-three syntax guard is polynomial-time.

theorem Cslib.Complexity.PositiveOneInExactThreeSATThree.syntaxCheck_iff (φ : Logic.PL.CNF ℕ) : syntaxCheck φ = true ↔ (∀ c ∈ φ, List.length c = 3 ∧ (List.map Prod.fst c).Nodup) ∧ OneSAT.positiveCheck φ = true ∧ ∀ (v : ℕ), List.count v φ.vars ≤ 3

The bounded exact-three guard checks exactly the syntactic restrictions.

theorem Cslib.Complexity.PositiveOneInExactThreeSATThree.mem_iff_syntaxCheck (φ : Logic.PL.CNF ℕ) : φ ∈ PositiveOneInExactThreeSATThree ↔ syntaxCheck φ = true ∧ φ ∈ OneSAT

Membership is the syntax guard together with exact-one satisfiability.

theorem Cslib.Complexity.PositiveOneInExactThreeSATThree.mem_NP : PositiveOneInExactThreeSATThree ∈ NP encCNF

Positive exact-three exact-one satisfiability with occurrence bound three belongs to NP.

def Cslib.Complexity.SharpOneSAT (φ : Logic.PL.CNF ℕ) : ℕ

Count exact-one models on the occurring variables, without a syntax restriction.

def Cslib.Complexity.SharpPositiveOneInThreeSAT (φ : Logic.PL.CNF ℕ) : ℕ

Count positive width-three exact-one models, returning zero on other syntax.

def Cslib.Complexity.SharpPositiveOneInExactThreeSAT (φ : Logic.PL.CNF ℕ) : ℕ

Count positive exact-three exact-one models, returning zero on other syntax.

def Cslib.Complexity.SharpPositiveOneInThreeSATThree (φ : Logic.PL.CNF ℕ) : ℕ

Count positive width-three, occurrence-three exact-one models; reject other syntax.

def Cslib.Complexity.SharpPositiveOneInExactThreeSATThree (φ : Logic.PL.CNF ℕ) : ℕ

Count positive exact-three, occurrence-three exact-one models; reject other syntax.

theorem Cslib.Complexity.SharpOneSAT.mem_OneSAT_iff {φ : Logic.PL.CNF ℕ} : φ ∈ OneSAT ↔ 0 < SharpOneSAT φ

Exact-one satisfiability is equivalent to a positive exact-one model count.

theorem Cslib.Complexity.SharpPositiveOneInThreeSAT.mem_PositiveOneInThreeSAT_iff {φ : Logic.PL.CNF ℕ} : φ ∈ PositiveOneInThreeSAT ↔ 0 < SharpPositiveOneInThreeSAT φ

Membership in the positive width-three language is positivity of its guarded count.

theorem Cslib.Complexity.SharpPositiveOneInExactThreeSAT.mem_PositiveOneInExactThreeSAT_iff {φ : Logic.PL.CNF ℕ} : φ ∈ PositiveOneInExactThreeSAT ↔ 0 < SharpPositiveOneInExactThreeSAT φ

Membership in the positive exact-three language is positivity of its guarded count.

theorem Cslib.Complexity.SharpPositiveOneInThreeSATThree.mem_PositiveOneInThreeSATThree_iff {φ : Logic.PL.CNF ℕ} : φ ∈ PositiveOneInThreeSATThree ↔ 0 < SharpPositiveOneInThreeSATThree φ

Membership in the positive width-three, occurrence-three language is a positive count.

theorem Cslib.Complexity.SharpPositiveOneInExactThreeSATThree.mem_PositiveOneInExactThreeSATThree_iff {φ : Logic.PL.CNF ℕ} : φ ∈ PositiveOneInExactThreeSATThree ↔ 0 < SharpPositiveOneInExactThreeSATThree φ

Membership in the positive exact-three, occurrence-three language is a positive count.