1package solver23// A CardConstr is a cardinality constraint, i.e a set of literals (represented with integer variables) associated with a minimal number of literals that must be true.4// A propositional clause (i.e a disjunction of literals) is a cardinality constraint with a minimal cardinality of 1.5type CardConstr struct {6 Lits []int7 AtLeast int8}910// AtLeast1 returns a cardinality constraint stating that at least one of the given lits must be true.11// This is the equivalent of a propositional clause.12func AtLeast1(lits ...int) CardConstr {13 return CardConstr{Lits: lits, AtLeast: 1}14}1516// AtMost1 returns a cardinality constraint stating that at most one of the given lits can be true.17func AtMost1(lits ...int) CardConstr {18 negated := make([]int, len(lits))19 for i, lit := range lits {20 negated[i] = -lit21 }22 return CardConstr{Lits: negated, AtLeast: len(lits) - 1}23}2425// Exactly1 returns two cardinality constraints stating that exactly one of the given lits must be true.26func Exactly1(lits ...int) []CardConstr {27 return []CardConstr{AtLeast1(lits...), AtMost1(lits...)}28}