Module satoxid::constraints

Collection of commonly used constraints.

Structs

And	Constraint which requires all literals to be true.
AtLeastK	This constraint encodes the requirement that at least k of lits are true.
AtMostK	This constraint encodes the requirement that at most k of lits are true.
Equal	Constraint which requires all literals to be same value.
ExactlyK	This constraint encodes the requirement that exactly k of lits are true.
Expr	Tseytin Encoding of propositional logic formulas.
If	Implication constraint. If cond is satisfied true then the then constraint has to be true.
LessCardinality	Constraint which encodes that fewer literals are true in smaller than in larger.
Not	Constraint which inverts a constraint. If a constraint C is unsatisfiable than Not(C) is satisfiable and vice versa.
Or	Constraint which represents a simple clause.
SameCardinality	Constraint to ensure that several sets of literals have all the same number of true literals.