@@ -56,3 +56,16 @@ Thus, for every variable $i$ we will either have $i$ in the returned list if the
**Caveat: In the SAT-community the term _model_ is used to describe an assignment, while we use the term as in the OR-community to describe the problem encoding.**
### Cardinality Constraints
When modelling some problem with boolean formulas, a frequent challenge is to model some cardinality constraints, i.e., from a set $L$ of literals, only at most $k$ are allowed to be satisfied.
For example, a tree should have at most $n-1$ edges selected.
If we interpret $\texttt{false}=0$ and $\texttt{true}=1$ (as commonly done in most programming languages), we can write these constraints as
\[\sum\limits_{\ell \in L} \ell \leq k\]
Such a constraint is called *cardinality constraint*.
As this is a very common constraint, some SAT-solvers (e.g., the previously used *Gluecard4*) support them directly (on top of the classical conjunctive normal form).
There are also automatic encodings that can convert cardinality constraints, but this is usually less efficient than telling the solver directly about the cardinality constraint, allowing it to use specialized algorithms.
