Documentation

CslibFrontier.Computability.Complexity.Problems.ThreeSATThree.Syntax

A native syntax guard for finite 3SAT-3 #

The scan checks clause widths and counts literal positions, including repetitions. It makes no satisfiability or planarity assertion. Total reductions use it to reject inputs outside their source syntax.

Main definitions #

Main results #

References #

Uses the existing CNF list representation and binary formula encoding.

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

Check width and literal-occurrence bounds three, independently of satisfiability.

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

    The finite scan checks exactly the two syntactic restrictions of 3SAT-3.

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

    The syntactic guard is computed in native polynomial time under binary CNF encoding.