diff --git a/sheets/03_card_sat/README.md b/sheets/03_card_sat/README.md
index 8271efadebd5a29fb680cd6a54265342cd069a20..4a27ed48b7b27b63397984c0645c4eeb62a581a7 100644
--- a/sheets/03_card_sat/README.md
+++ b/sheets/03_card_sat/README.md
@@ -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.
+