Hard formula generator (pysat.examples.genhard)#
List of classes#
Mutilated chessboard principle (CB). |
|
Generator of ordering (or greater than, GT) principle formulas. |
|
Generator of the parity principle (PAR) formulas. |
|
Generator of \(k\) pigeonhole principle (\(k\)-PHP) formulas. |
Module description#
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
$ genhard.py -t php -n 3 -v
c PHP formula for 4 pigeons and 3 holes
c (pigeon, hole) pair: (1, 1); bool var: 1
c (pigeon, hole) pair: (1, 2); bool var: 2
c (pigeon, hole) pair: (1, 3); bool var: 3
c (pigeon, hole) pair: (2, 1); bool var: 4
c (pigeon, hole) pair: (2, 2); bool var: 5
c (pigeon, hole) pair: (2, 3); bool var: 6
c (pigeon, hole) pair: (3, 1); bool var: 7
c (pigeon, hole) pair: (3, 2); bool var: 8
c (pigeon, hole) pair: (3, 3); bool var: 9
c (pigeon, hole) pair: (4, 1); bool var: 10
c (pigeon, hole) pair: (4, 2); bool var: 11
c (pigeon, hole) pair: (4, 3); bool var: 12
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
Alternatively, each of the considered problem encoders can be accessed with
the use of the standard import interface of Python, e.g.
>>> from pysat.examples.genhard import PHP
>>>
>>> cnf = PHP(3)
>>> print(cnf.nv, len(cnf.clauses))
12 22
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.
Module details#
- class examples.genhard.CB(*args, **kwargs)#
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
exhaustivethe 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
- Returns:
object of class
pysat.formula.CNF.
- class examples.genhard.GT(*args, **kwargs)#
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
- Returns:
object of class
pysat.formula.CNF.
- class examples.genhard.PAR(*args, **kwargs)#
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
- Returns:
object of class
pysat.formula.CNF.
- class examples.genhard.PHP(*args, **kwargs)#
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
- Returns:
object of class
pysat.formula.CNF.