Polynomial-time exact-one encoding

The ordinary CNF encoding of exact-one semantics enumerates pairs of literal positions. Its construction is polynomial-time under the existing list and literal encodings. This is a semantic bridge, separate from the positive exact-three reduction.

Main results

• Clause.computableInPolyTime_oneEncoding: encode one exact-one clause.
• CNF.computableInPolyTime_oneEncoding: encode an exact-one formula.

References

These are original computational certificates for the existing positional encoding.

theorem Cslib.Logic.PL.Clause.atMostOneOccurrences_eq_flatMap {V : Type} (c : Clause V) : c.atMostOneOccurrences = List.flatMap (fun (p : Literal V × ℕ) => List.map (fun (l : Std.Sat.Literal V) => [Std.Sat.Literal.negate p.1, l.negate]) (List.drop (p.2 + 1) c)) (List.zipIdx c)

Enumerate each later literal position after its first position.

theorem Cslib.Logic.PL.Clause.computableInPolyTime_atMostOneOccurrences {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime atMostOneOccurrences (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)))

The positional pair clauses can be emitted in polynomial time.

theorem Cslib.Logic.PL.Clause.computableInPolyTime_oneEncoding {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime oneEncoding (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)))

Exact-one clause encoding is polynomial-time for any fixed variable encoding.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_oneEncoding {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime oneEncoding (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool)))

Exact-one formula encoding is polynomial-time for any fixed variable encoding.

def Cslib.Logic.PL.CNF.FromSAT.encVariable {V : Type} (enc : V ↪ List Bool) : Variable V ↪ List Bool

Source labels retain their encoding; local clause and slot indices are unary.

theorem Cslib.Logic.PL.CNF.FromSAT.computableInPolyTime_clause {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime (fun (p : ℕ × Clause V) => clause p.1 p.2) (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair (encVariable enc) Turing.MultiTapeTM.encBool)))

One ordinary-clause replacement is native polynomial-time.

theorem Cslib.Logic.PL.CNF.FromSAT.computableInPolyTime_formula {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime formula (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair (encVariable enc) Turing.MultiTapeTM.encBool)))

The ordinary clause replacements are polynomial-time under the original label encoding.

def Cslib.Logic.PL.CNF.PositiveExactOne.encVariable {V : Type} (enc : V ↪ List Bool) : Variable V ↪ List Bool

Source labels retain their encoding; clause, literal, and auxiliary positions are unary.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.computableInPolyTime_formula {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime formula (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair (encVariable enc) Turing.MultiTapeTM.encBool)))

Eliminating all negative occurrences is native polynomial-time.

def Cslib.Logic.PL.CNF.PositiveExactOneCompile.encVariable {V : Type} (enc : V ↪ List Bool) : Variable V ↪ List Bool

The two local auxiliary families use unary indices and retain the source label encoding.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.computableInPolyTime_rawFormula {V : Type} (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime rawFormula (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair (encVariable enc) Turing.MultiTapeTM.encBool)))

Composing the two local replacements is native polynomial-time.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.computableInPolyTime_formula {V : Type} [DecidableEq V] (enc : V ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime formula (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encBool)))

Compact output labels are computed as bounded unary ranks, then encoded in binary.