# Hard formula generator (pysat.examples.genhard)#

## List of classes#

 CB Mutilated chessboard principle (CB). GT Generator of ordering (or greater than, GT) principle formulas. PAR Generator of the parity principle (PAR) formulas. PHP 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.

1

Stephen A. Cook, Robert A. Reckhow. The Relative Efficiency of Propositional Proof Systems. J. Symb. Log. 44(1). 1979. pp. 36-50

2(1,2)

Balakrishnan Krishnamurthy. Short Proofs for Tricky Formulas. Acta Informatica 22(3). 1985. pp. 253-275

3(1,2)

Michael Alekhnovich. Mutilated Chessboard Problem Is Exponentially Hard For Resolution. Theor. Comput. Sci. 310(1-3). 2004. pp. 513-525

4(1,2)

Miklós Ajtai. Parity And The Pigeonhole Principle. Feasible Mathematics. 1990. pp. 1–24

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(size, exhaustive=False, topv=0, verb=False)#

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

Returns

object of class pysat.formula.CNF.

class examples.genhard.GT(size, topv=0, verb=False)#

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.

5

Gunnar Stålmarck. Short Resolution Proofs for a Sequence of Tricky Formulas. Acta Informatica. 33(3). 1996. pp. 277-280

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(size, topv=0, verb=False)#

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(nof_holes, kval=1, topv=0, verb=False)#

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.

6

Armin Haken. The Intractability of Resolution. Theor. Comput. Sci. 39. 1985. pp. 297-308

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.