2-satisfiability

Definition2-SAT as a decision problem#✓fully proved

The 2-SAT decision problem accepts a bitstring \(x\) exactly when \(x\) decodes, under the canonical bitstring encoding, to a pair \((n, \varphi)\) of a natural number \(n\) and a CNF formula \(\varphi\) such that every clause of \(\varphi\) has at most two literals, every variable occurring in \(\varphi\) is less than \(n\), and there is a list \((a_0, \dots, a_{n-1})\) of booleans such that \(\varphi\) is satisfied by the assignment that sends each variable \(v < n\) to \(a_v\) and every other variable to false.

noncomputable def twoSatDec :
    MetaMathlibExt.ComplexityTheory.DecisionProblem := fun x =>
  match MetaMathlibExt.BitstringEncoding.bitDecode
      (α := ℕ × Cslib.Logic.PL.CNF) x with
  | some i => decide (
      (∀ clause ∈ i.2, clause.length ≤ 2 ∧ ∀ l ∈ clause, l.1 < i.1) ∧
      ∃ assign : List Bool, assign.length = i.1 ∧
        Cslib.Logic.PL.CNF.Satisfies (fun v => assign.getD v false) i.2)
  | none => false

Uses 12 · Used by 1

Statement usesCNF formula · Satisfaction of a CNF formula · CNF clause · Bitstring encodings · Decoding function of a bitstring encoding · Decoding inverts bitstring encoding · Encoding function of a bitstring encoding · Self-delimiting form of a bitstring · Parsing one self-delimiting block · Parsing a list of booleans into self-delimiting blocks · Bounded parsing of self-delimiting blocks · Decision problems

Used by2-SAT is in P

Theorem2-SAT is in P#●ready to prove

The 2-SAT decision problem lies in the complexity class P.

public theorem_wanted two_sat_in_p :
    twoSatDec ∈ MetaMathlibExt.ComplexityTheory.P

Sources

• M. Davis, G. Logemann, and D. Loveland, "A machine program for theorem-proving", Communications of the ACM 5 (1962), 394-397; B. Aspvall, M. F. Plass, and R. E. Tarjan, "A linear-time algorithm for testing the truth of certain quantified Boolean formulas", Information Processing Letters 8 (1979), 121-123.

Uses 4

Statement uses2-SAT as a decision problem · Complexity classes · Decision problems · The complexity class P

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.