Documentation

CslibFrontier.Computability.Complexity.Problems.CSP.Basic

Native satisfiability for fixed finite Boolean constraint languages #

Cslib.Complexity.CSPSAT arity sem contains exactly the well-formed satisfiable instances in the existing CSP representation, with variables numbered by arbitrary natural numbers. Its encoding is the existing encCSP encRel encNat: framed lists/pairs and binary variable indices. The relation alphabet, its encoding, arities and semantics are fixed independently of the instance [Che06], Definitions 3.1–3.3. Repeated variables and empty scopes are allowed; incorrect scope lengths are rejected, and empty relations are interpreted as false.

For every finite relation alphabet this problem belongs to native NP. The proof compiles forbidden local assignments to CNF using the existing fixed-width polynomial-time compiler; malformed inputs produce an empty clause. No uniform bound in the size of the language is claimed.

Main definitions #

Main results #

source
def Cslib.Complexity.CSPSAT {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) :
Set (Logic.PL.CSP Rel ℕ)

The well-formed satisfiable instances of a fixed Boolean constraint language.

Instances For
    source
    theorem Cslib.Complexity.CSPSAT.mem_iff {Rel : Type} (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (F : Logic.PL.CSP Rel ℕ) :
    F ∈ CSPSAT arity sem ↔ Logic.PL.CSP.WellFormed arity F ∧ Logic.PL.CSP.Satisfiable sem F

    Membership separates exact-arity syntax from satisfiability.

    source
    theorem Cslib.Complexity.CSPSAT.polyTimeReducible_of_guard {Rel : Type} [Finite Rel] {β : Type} {encB : β ↪ List Bool} {B : Set β} (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) {compile : Logic.PL.CSP Rel ℕ → β} (reject : β) (hcompile : Turing.MultiTapeTM.ComputableInPolyTime compile (encCSP encRel Turing.MultiTapeTM.encNat) encB) (hcorrect : ∀ (F : Logic.PL.CSP Rel ℕ), Logic.PL.CSP.WellFormed arity F → (Logic.PL.CSP.Satisfiable sem F ↔ compile F ∈ B)) (hreject : reject ∉ B) :
    PolyTimeReducible (encCSP encRel Turing.MultiTapeTM.encNat) encB (CSPSAT arity sem) B

    Guarded compilation. A polynomial-time compiler that is faithful on well-formed instances, followed by an exact-arity guard sending every malformed instance to a fixed instance outside the target, reduces CSPSAT to the target.

    source
    theorem Cslib.Complexity.CSPSAT.mem_NP {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) :
    CSPSAT arity sem ∈ NP (encCSP encRel Turing.MultiTapeTM.encNat)

    Every fixed finite Boolean constraint language has a native NP satisfiability problem, under framed list/pair encodings with binary variable indices.