Tractability from a common Boolean constant #
A fixed finite Boolean constraint language preserved by either unary constant has a native polynomial-time satisfiability problem. The decider checks exact arities and rejects constraints using an empty relation. Otherwise the common constant satisfies the whole instance. This includes empty and nullary relations and arbitrary binary variable labels.
These are the first two cases of [Che06], Theorem 3.20. Testing relation nonemptiness is fixed preprocessing of a finite alphabet, not a uniform solver for supplied truth tables.
Main results #
Cslib.Complexity.CSPSAT.mem_P_of_constant: native P from a common unary constant.
theorem Cslib.Complexity.CSPSAT.mem_P_of_constant {Rel : Type} [Finite Rel] (encRel : Rel ↪ List Bool) (arity : Rel → ℕ) (sem : Rel → List Bool → Bool) (b : Bool) (hb : Logic.PL.CSP.HasPolymorphism arity sem fun (x : Fin 1 → Bool) => b) :
A common unary constant gives native polynomial-time satisfiability for a fixed finite Boolean constraint language. Empty relations are rejected before applying the constant model.