========================================================================= 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] ]) ) [] =========================================================================