def Trestle.Encode.Cardinality.naiveLtK.cond {ν : Type} (cond : Clause (Literal ν)) (k : ℕ) (lits : Array (Literal ν)) : VEncCNF ν Unit ((fun (τ : Model.PropAssignment ν) => τ ⊨ cond.toPropFun)ᶜ ⇨ lessThan k ↑lits.toList)

Conditional, naive less-than-k encoding, using (n choose k) clauses. This is identical to naiveLtK, but accepts an array of literals to be prepended to every clause.

Equations

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

def Trestle.Encode.Cardinality.naiveLtK {ν : Type} (k : ℕ) (lits : Array (Literal ν)) : VEncCNF ν Unit (lessThan k ↑lits.toList)

Naive less-than-k encoding, using (n choose k) clauses.

Equations

• Trestle.Encode.Cardinality.naiveLtK k lits = Trestle.Encode.VEncCNF.mapProp ⋯ (Trestle.Encode.Cardinality.naiveLtK.cond #[] k lits)

def Trestle.Encode.Cardinality.naiveAtLeastK.cond {ν : Type} (cond : Clause (Literal ν)) (k : ℕ) (lits : Array (Literal ν)) : VEncCNF ν Unit ((fun (τ : Model.PropAssignment ν) => τ ⊨ cond.toPropFun)ᶜ ⇨ atLeast k ↑lits.toList)

Conditional, naive at-least-k encoding

Equations

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

def Trestle.Encode.Cardinality.naiveAtLeastK {ν : Type} (k : ℕ) (lits : Array (Literal ν)) : VEncCNF ν Unit (atLeast k ↑lits.toList)

Conditional, naive at-least-k encoding

Equations

• Trestle.Encode.Cardinality.naiveAtLeastK k lits = Trestle.Encode.VEncCNF.mapProp ⋯ (Trestle.Encode.Cardinality.naiveAtLeastK.cond #[] k lits)

@[inline]

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

Trivial at least one encoding (just a single clause)

Equations

• Trestle.Encode.Cardinality.atLeastOne lits = Trestle.Encode.VEncCNF.mapProp ⋯ (Trestle.Encode.VEncCNF.addClause lits)