theorem Trestle.Encode.Cardinality.amo_iff {ν : Type u_1} (lits : Array (Literal ν)) (τ : Model.PropAssignment ν) : atMost 1 (↑lits.toList) τ ↔ ∀ (i : ℕ) (x : i < lits.size) (j : ℕ) (x_1 : j < lits.size), τ ⊨ LitVar.toPropFun lits[i] → τ ⊨ LitVar.toPropFun lits[j] → i = j

def Trestle.Encode.Cardinality.amoPairwise {ν : Type} (lits : Array (Literal ν)) : VEncCNF ν Unit (atMost 1 ↑lits.toList)

The pairwise at-most-one encoding.

An O(n²) encoding comprising binary clauses of every pair of literals. Formally,

∀ x,y ∈ lits, x ≠ y → (¬x ∨ ¬y)

The only way to satisfy the encoding is to never have any pair of literals both set to false in the assignment. Thus, at most one literal is true.

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Trestle.Encode.Cardinality.amoCut4 {ν : Type} (lits : Array (Literal ν)) (k : ℕ := 3) (hk : k ≥ 2 := by decide) : VEncCNF ν Unit (atMost 1 ↑lits.toList)

The cut4 at-most-one encoding.

An O(n) encoding constructed by repeatedly taking the first k literals from the list l such that

l = a ++ b, |a| = k

and replacing a with a temporary variable t that is true when any literal in a is true. This forces the remaining literals in b to be false, if the overall AMO constraint is to be satisfied.

Equations

• One or more equations did not get rendered due to their size.

def Trestle.Encode.Cardinality.amoOrdEncoding {ν : Type} (lits : Array (Literal ν)) : VEncCNF ν Unit (atMost 1 ↑lits.toList)

The order encoding, except we do not substitute the literals.

Equations

• One or more equations did not get rendered due to their size.