Satisfiability Problem · Formal Verification and Proof Systems

Lesson 6

Nikolai Chukhin · Alexander S. Kulikov

There are known comparatively simple formulas for which any resolution proof is exponentially long. One such formula encodes the pigeonhole principle: let the variable \(x_{ph}\), where \(1 \le p \le n+1\) and \(1 \le h \le n\), be equal to one if and only if the \(p\)-th pigeon sits in the \(h\)-th hole. The formula consists of the following clauses.

  • Every pigeon sits somewhere: for all \(1 \le p \le n+1\) \[(x_{p1}\lor x_{p2}\lor \dotsb \lor x_{pn})\ .\]

  • In each hole at most one pigeon sits: for all \(1 \le h \le n\) and all \(1 \le p \neq p' \le n+1\) \[(\overline{x_{ph}}\lor \overline{x_{p'h}}) \ .\]

One can see that this formula is hard for SAT solvers by running the code below. It won’t finish even in an hour. 

from pysat.solvers import Solver
from pysat.card import *
from pysat.formula import IDPool, CNF

n = 20
pigeons, holes = range(n + 1), range(n)
pool, formula = IDPool(), CNF()

for p in pigeons:
    formula.extend(CardEnc.atleast(lits=[pool.id((p, h)) for h in holes], bound=1, vpool=pool))

for h in holes:
    formula.extend(CardEnc.atmost(lits=[pool.id((p, h)) for p in pigeons], bound=1, vpool=pool))

solver = Solver(bootstrap_with=formula)
solver.solve()
As you can see, we set constraints using the built-in methods \(\texttt{atleast}\) and \(\texttt{atmost}\). And the object \(\texttt{pool}\) itself issues integer identifiers to variables: \(\texttt{pool.id(obj)}\) checks if the object \(\texttt{obj}\) already has an identifier (if yes, it simply returns it; if not, it assigns, saves, and returns it). In the methods \(\texttt{atmost}\)/\(\texttt{atleast}\) it is important to pass the \(\texttt{pool}\) object, because these methods may introduce new variables when writing constraints (to use fewer clauses).

The \(\texttt{PySAT}\) module also has a built-in generator for such a formula. 

from pysat.solvers import Solver
from pysat.examples.genhard import PHP

solver = Solver(bootstrap_with=PHP(nof_holes=20))
solver.solve()