=========================================================================
Advanced Topics in Computational Social Choice 2021
Calling Lingeling from Python via PyLGL
Ulle Endriss, September 2021
=========================================================================
Lingeling is one of the best-performing SAT solvers available and the
Python module pylgl provides a simple interface for accessing the solver
directly from Python.
Make sure you have Python3 installed on your laptop. If you are not sure
how to do this, probably this will work:
https://www.python.org/downloads/
Then install pylgl:
https://pypi.python.org/pypi/pylgl/
You can use this tool to check whether a given formula in CNF is
satisfiable. If it is, one of the models satisfying the formula will be
returned. You can also generate the list of all models that satisfy your
formula (this might be slow for formulas with very many models). Clauses
are represented as lists of positive and negative integers, representing
positive and negative literals. A formula in CNF then is represented as a
list of such lists. Thus, the formula (P \/ Q) /\ (-P \/ -Q \/ R) would
be represented as [ [1,2], [-1,-2,3] ].
After you have started up Python3, run the following command to make the
functions solve() and itersolve() available to you:
>>> from pylgl import solve, itersolve
Now you can use the function solve() to confirm that the formula
(P \/ Q) /\ (-P \/ -Q \/ R) is satisfiable and to compute one of its
models (the first one the system happens to find):
>>> solve([ [1,2], [-1,-2,3] ])
[1, 2, 3]
Thus, if we set all three variable to TRUE, then our formula is
satisfied. Note that in the input a list such as [-1,-2,3] denotes a
disjunction, while in the output a list denotes a model (which you might
think of as a conjunction of literals).
Suppose you want to compute a second model of the same formula. One way
of doing this would be to add one further clause to the CNF that
explicitly rules out the first model we found:
>>> solve([ [1,2], [-1,-2,3], [-1,-2,-3] ])
[1, -2, -3]
So another way of satisfying the formula (P \/ Q) /\ (-P \/ -Q \/ R)
would be to set P to TRUE and the other two variables to FALSE.
The next example shows that the formula
(P \/ Q) /\ (-P \/ Q) /\ (P \/ -Q) /\ (-P \/ -Q) is not satisfiable:
>>> solve([ [1,2], [-1,2], [1,-2], [-1,-2] ])
'UNSAT'
You can use the function itersolve() to compute all of the models of a
given formula. Note that you need to use the function list() to transform
the output into a list that can be displayed:
>>> list( itersolve([ [1,2], [-1,-2,3] ]) )
[[1, 2, 3], [1, -2, 3], [-1, 2, 3], [-1, 2, -3], [1, -2, -3]]
>>> list( itersolve([ [1,2], [-1,-2,3], [-1,-2,-3] ]) )
[[1, -2, -3], [-1, 2, -3], [-1, 2, 3], [1, -2, 3]]
>>> list( itersolve([ [1,2], [-1,2], [1,-2], [-1,-2] ]) )
[]
=========================================================================