This module is designed to provide a few examples illustrating how PySAT
can be used for encoding practical problems into CNF formulas. These
include combinatorial principles that are widely studied from the
propositional proof complexity perspective. Namely, encodings for the
following principles are implemented: pigeonhole principle (PHP)
[1], ordering (greater-than) principle (GT) [2], mutilated
chessboard principle (CB) [3], and parity principle
(PAR) [4].
The module can be used as an executable (the list of available command-line
options can be shown using genhard.py-h) in the following way
Given this example, observe that classes PHP, GT,
CB, and PAR inherit from class
pysat.formula.CNF and, thus, their corresponding clauses can
accessed through variable .clauses.
Mutilated chessboard principle (CB). Given an integer \(n\), the
principle states that it is impossible to cover a chessboard of size
\(2n\cdot 2n\) by domino tiles if two diagonally opposite corners
of the chessboard are removed.
Note that the chessboard has \(4n^2-2\) cells. Introduce a Boolean
variable \(x_{ij}\) for \(i,j\in[4n^2-2]\) s.t. cells \(i\)
and \(j\) are adjacent (no variables are introduced for pairs of
non-adjacent cells). CB formulas comprise clauses (1)
\((\neg{x_{ji} \vee \neg{x_{ki}}})\) for every \(i,j \neq
k\) meaning that no more than one adjacent cell can be paired with the
current one; and (2) \((\vee_{j \in \text{Adj}(i)} {x_{ij}})\,\,
\forall i\) enforcing that every cell \(i\) should be paired with
at least one adjacent cell.
Clearly, since the two diagonal corners are removed, the formula is
unsatisfiable. Also note the following. Assuming that the number of
black cells is larger than the number of the white ones, CB formulas
are unsatisfiable even if only a half of the formula is present, e.g.
when \(\textsf{AtMost1}\) constraints are formulated only for the
white cells while the \(\textsf{AtLeast1}\) constraints are
formulated only for the black cells. Depending on the value of
parameter exhaustive the encoder applies the complete or
partial formulation of the problem.
Mutilated chessboard principle is known to be hard for resolution [3].
Parameters:
size (int) – problem size (\(n\))
exhaustive (bool) – encode the problem exhaustively
topv (int) – current top variable identifier
verb (bool) – defines whether or not the encoder is verbose
Generator of ordering (or greater than, GT) principle formulas. Given
an integer parameter \(n\), the principle states that any partial
order on the set \(\{1,2,\ldots,n\}\) must have a maximal element.
Assume variable \(x_{ij}\), for \(i,j\in[n],i\neq j\), denotes
the fact that \(i \succ j\). Clauses \((\neg{x_{ij}} \vee
\neg{x_{ji}})\) and \((\neg{x_{ij}} \vee \neg{x_{jk}} \vee
x_{ik})\) ensure that the relation \(\succ\) is anti-symmetric and
transitive. As a result, \(\succ\) is a partial order on
\([n]\). The additional requirement that each element \(i\) has
a successor in \([n]\setminus\{i\}\) represented a clause
\((\vee_{j \neq i}{x_{ji}})\) makes the formula unsatisfiable.
GT formulas were originally conjectured [2] to be hard for resolution.
However, [5] proved the existence of a polynomial size resolution
refutation for GT formulas.
Parameters:
size (int) – number of elements (\(n\))
topv (int) – current top variable identifier
verb (bool) – defines whether or not the encoder is verbose
Generator of the parity principle (PAR) formulas. Given an integer
parameter \(n\), the principle states that no graph on \(2n+1\)
nodes consists of a complete perfect matching.
The encoding of the parity principle uses \(\binom{2n+1}{2}\)
variables \(x_{ij},i \neq j\). If variable \(x_{ij}\) is
true, then there is an edge between nodes \(i\) and \(j\).
The formula consists of the following clauses: \((\vee_{j \neq
i}{x_{ij}})\) for every \(i\in[2n+1]\), and \((\neg{x_{ij}}
\vee \neg{x_{kj}})\) for all distinct \(i,j,k \in [2n+1]\).
The parity principle is known to be hard for resolution [4].
Parameters:
size (int) – problem size (\(n\))
topv (int) – current top variable identifier
verb (bool) – defines whether or not the encoder is verbose
Generator of \(k\) pigeonhole principle (\(k\)-PHP) formulas.
Given integer parameters \(m\) and \(k\), the \(k\)
pigeonhole principle states that if \(k\cdot m+1\) pigeons are
distributes by \(m\) holes, then at least one hole contains more
than \(k\) pigeons.
Note that if \(k\) is 1, the principle degenerates to the
formulation of the original pigeonhole principle stating that
\(m+1\) pigeons cannot be distributed by \(m\) holes.
Assume that a Boolean variable \(x_{ij}\) encodes that pigeon
\(i\) resides in hole \(j\). Then a PHP formula can be seen as
a conjunction: \(\bigwedge_{i=1}^{k\cdot
m+1}{\textsf{AtLeast1}(x_{i1},\ldots,x_{im})}\wedge
\bigwedge_{j=1}^{m}{\textsf{AtMost}k(x_{1j},\ldots,x_{k\cdot
m+1,j})}\). Here each \(\textsf{AtLeast1}\) constraint forces every
pigeon to be placed into at least one hole while each
\(\textsf{AtMost}k\) constraint allows the corresponding hole to
have at most \(k\) pigeons. The overall PHP formulas are
unsatisfiable.
PHP formulas are well-known [6] to be hard for resolution.
Parameters:
nof_holes (int) – number of holes (\(n\))
kval (int) – multiplier \(k\)
topv (int) – current top variable identifier
verb (bool) – defines whether or not the encoder is verbose