3.1.6. cnfgen.families.pigeonhole module¶
Pigeonhole principle formulas
The pigeonhole principle \(\mathsf{PHP}_{n}^{m}\), written in conjunctive normal form, is a propositional formula which claims that it is possible to place \(m\) pigeons into \(n\) holes without collisions, whenever \(m > n\).
Pigeonhole principle formulas are classic benchmarks for SAT solving and for Resolution proof systems. The module contains the implementation of several variants of this formulas.
The most classic pigeonhole principle formula \(\mathsf{PHP}_{n}^{n+1}\) was the first CNF proved to be hard for resolution [H85].
| [H85] | Haken, A. (1985). The intractability of resolution. Theoretical Computer Science, 39, 297–308. |
-
BinaryPigeonholePrinciple(pigeons, holes)¶ Binary Pigeonhole Principle CNF formula
The binary pigeonhole principle CNF formula claims that that it is possibile to place \(m\) pigeons into \(n\) holes without collisions. This is clearly impossible whenever \(m > n\).
This formula encodes the principle using binary strings to identify the holes. Let \(b\) the smallest number of bits sufficient to encode in binary all values from \(0\) to \(n-1\). For every \(i \in [m]\) there are \(b\) dedicated boolean variables encoding the hole where the pigeon \(i\) flies.
Parameters: - pigeon: int
number of pigeons (must be >=0).
- hole: int
number of holes (must be >=0).
Returns: cnfgen.formula.cnf.CNFA CNF formulas encoding binary the pigeonhole principle.
Raises: - TypeError
If either pigeons or holes is not an integer number.
- ValueError
If either pigeons or holes is less than zero.
-
GraphPigeonholePrinciple(G, functional=False, onto=False)¶ Graph Pigeonhole Principle CNF formula
The graph pigeonhole principle CNF formula, defined on a bipartite graph \(G=(L,R,E)\), is a variant of the pigeonhole principle where the left vertices \(L\) are the pigeons, the right vertices \(R\) are the holes. The formula claims that there is a subset of edges \(E' \subseteq E\) such that every vertex in \(u \in L\) has at least one incident edge in \(E'\) and every \(v \in R\) has at most one incident edge in \(E'\).
The formula is satisfiable if and only if the graph has a matching of size \(|L|\).
The formula is encoded with variables \(p_{u,v}\) for \(u \in L\) and \(v \in R\) where the intended meaning is that \(p_{u,v}\) is True when pigeon \(u\) flies into hole \(v\). There are different variants of this formula, depending on the values of functional and onto argument.
- PHP(G): each \(u \in L\) can fly to multiple \(v \in R\)
- FPHP(G): each \(u \in L\) can fly to exactly one \(v \in R\)
- onto-PHP: each \(v \in R\) must get a pigeon
- matching: \(E'\) must be a perfect matching
Parameter G can be either of type
cnfgen.graphs.BipartiteGraphor of type anetworkx.graph. In the latter case it must be a correct representation of a bipartite graph according to [NetworkX].Parameters: - G :
cnfgen.graphs.BipartiteGraphornetworkx.graph the bipartite graph describing the possible pairings
- functional: bool
enforce at most one edge per left vertex
- onto: bool
enforce that any right vertex has one incident edge
Returns: cnfgen.formula.cnf.CNFA CNF formulas encoding the graph pigeonhole principle.
Raises: - TypeError
G is neither a
cnfgen.graphs.BipartiteGraphnor anetworkx.graph- ValueError
G is not a proper bipartite graph
References
-
PigeonholePrinciple(pigeons, holes, functional=False, onto=False)¶ Pigeonhole Principle CNF formula
The pigeonhole principle CNF formula claims that that it is possibile to place \(m\) pigeons into \(n\) holes without collisions. This is clearly impossible whenever \(m > n\).
The formula is encoded with variables \(p_{i,j}\) for \(i \in [m]\) and \(j \in [n]\) where the intended meaning is that \(p_{i,j}\) is True when pigeon \(i\) flies into hole \(j\). There are different variants of this formula, depending on the values of functional and onto argument.
- PHP: pigeon can sit in multiple holes
- FPHP: each pigeon sits in exactly one hole
- onto-PHP: pigeon can sit in multiple holes, every hole must be covered
- Matching: one-to-one bijection between pigeons and holes.
Parameters: - pigeon: int
number of pigeons (must be >=0).
- hole: int
number of holes (must be >=0).
- functional: bool, optional
enforce at most one hole per pigeon (default: False).
- onto: bool, optional
enforce that any hole must have a pigeon (default: False).
Returns: cnfgen.formula.cnf.CNFA CNF formulas encoding the pigeonhole principle.
Raises: - TypeError
If either pigeons or holes is not an integer number.
- ValueError
If either pigeons or holes is less than zero.
Examples
>>> print(PigeonholePrinciple(4,3).to_dimacs()) p cnf 12 22 1 2 3 0 4 5 6 0 7 8 9 0 10 11 12 0 -1 -4 0 -1 -7 0 -1 -10 0 -4 -7 0 -4 -10 0 -7 -10 0 -2 -5 0 -2 -8 0 -2 -11 0 -5 -8 0 -5 -11 0 -8 -11 0 -3 -6 0 -3 -9 0 -3 -12 0 -6 -9 0 -6 -12 0 -9 -12 0 <BLANKLINE>
-
RelativizedPigeonholePrinciple(pigeons, resting_places, holes)¶ Relativized Pigeonhole Principle CNF formula
This formula is a variant of the pigeonhole principle. We consider \(m\) pigeons, \(r\) resting places, and \(n\) holes. The formula claims that pigeons can fly into holes with no conflicts, with the additional caveat that before landing in a hole, each pigeon stops in some resting place. No two pigeons can rest in the same place.
The formula is encoded with variables \(p_{i,j}\) for \(i \in [m]\) and \(k \in [t]\), and variables \(q_{k,j}\) for \(k \in [t]\) and \(j \in [n]\). The intended meaning is that \(p_{i,k}\) is True when pigeon \(i\) rests into a resting place \(k\), and \(q_{k,j}\) is True when the pigeon resting at \(k\) flies into hole \(j\). The formula is only satisfiable when \(m \leq t \leq n\).
A more complete description of the formula can be found in [ALN16]
Parameters: - pigeons: int
number of pigeons (must be >=0).
- resting_places: int
number of resting places (must be >=0).
- holes: int
number of holes (must be >=0).
Returns: cnfgen.formula.cnf.CNFA CNF formulas encoding the pigeonhole principle.
Raises: - TypeError
If either pigeons, resting_places, or holes is not an integer number.
- ValueError
If either pigeons, resting_places, or holes is less than zero.
References
[ALN16] Atserias, A., Lauria, M., & Nordstr”om, Jakob (2016). Narrow Proofs May Be Maximally Long. ACM Transactions on Computational Logic, 17(3), 19–1–19–30. http://dx.doi.org/10.1145/2898435