A cardinality constraint of the form
A cardinality constraint of the form
sum(lits) relop k
. sum(lits) relop k }}}
A classic PB constraint f the form
A classic PB constraint f the form
sum(weights(lit)*lit) relop k
. sum(weights(lit)*lit) relop k }}}
Abstract type for relational operators used in cardinality constraints.
Adds a cardinality constraint
Adds a cardinality constraint
sum(lits) >= k
.
sum(lits) >= k }}}
optionally add a masking literal that allows to switch the clause on and off
if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.
Adds a cardinality constraint
Adds a cardinality constraint
sum(lits) <= k
.
sum(lits) <= k }}}
optionally add a masking literal that allows to switch the clause on and off
if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.
Adds a cardinality constraint with specified relop and constant to the solver.
Adds a cardinality constraint with specified relop and constant to the solver.
optional switch literal
if true and if switch is None, creates a fresh switch literal that allows to switch the constraint on and off
if switch is defined or if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.
Method to use to effectively add a cardinality constraint to the underlying Solver implementation.
Adds a cardinality constraint
Adds a cardinality constraint
sum(lits) <= k
.
sum(lits) <= k }}}
optionally add a masking literal that allows to switch the clause on and off
if switchable is true, Some(fresh) where fresh is a fresh literal that allows to switch the clause on or off, None otherwise.
an iterator on the cardinality constraints currently in the solver.
the number of cardinality constraints of the formula.
An interface for building pseudo-boolean problems on top of CNF formulas.