5

LINKS:
Z3 theorem prover
picosat with pyhton bindings

I've used Z3 as a SAT-solver. For larger formulae there seem to be performance issues which is why I wanted to check out picosat to see whether it's a faster alternative. My existing python code generates a propositional formula in z3 syntax:

from z3 import *

import pycosat
from pycosat import solve, itersolve

#
#1 2  3  4  5  6  7   8  (variable names in picosat are numbers!)
#
C, G, M, P, R, S, SN, B = Bools('C G M P R S SN B')
C = (And(*(S,Or(Not(S),P),Or(Not(P),S),Or(Not(P),B),Or(Not(C),P),Or(Not(G),P),Or(Not(M),P),Or(Not(R),P),Or(Not(SN),P),Or(Not(B),P),True,Not(False),Or(R,SN,B,G,M,C,True))))

# formula in Z3:
f = simplify(C)

print f

OUTPUT / RESULT

And(S,
    Or(Not(S), P),
    Or(Not(P), S),
    Or(Not(P), B),

    Or(Not(C), P),
    Or(Not(G), P),
    Or(Not(M), P),
    Or(Not(R), P),
    Or(Not(SN), P),
    Or(Not(B), P))

Picosat however uses lists/arrays of numbers, as shown in the following example ("clauses1": 6 refers to variable P, -6 means "not P" etc.):

import pycosat
from pycosat import solve, itersolve
#
# use pico sat
#
nvars = 8
clauses =[
    [6],
    [-6, 4],   ##  "Or(Not(S), P)" from OUPUT above
    [-4, 6],
    [-4, 8],
    [-1, 4],
    [-2, 4],
    [-3, 4],
    [-5, 4],
    [-7, 4],
    [-8, 4]]

#
# efficiently find all models of the formula
#
sols = list(itersolve(clauses, vars=nvars))
print "result:"
print sols
print "\n\n====\n"

What do you recommend as a simple solution to convert a Z3 variable (like the varaible "f" from the code example) representing a formula in CNF into the forementioned format picosat uses to represent formulae in CNF? I really tried to use the python API of Z3, however the documentation was not sufficient to solve the problem by myself.

(Please note the example above merely illustrates the concept. The formula represented by variable C would be dynamically generated and would be too complex to be processed efficiently by z3 directly)

mrsteve
  • 4,082
  • 1
  • 26
  • 63

1 Answers1

5

First, we should convert the Z3 formula into CNF. The following post address this issue

To convert the Z3 CNF formula into Dimacs, we can just write a function that traverses it and generate the list of list of integers. The following two posts describe how to traverse Z3 formulas

Finally, if you need maps from expressions to values, you can use the following approach

Community
  • 1
  • 1
Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • Do you know if picosat is reasonably efficient? Are there SAT solvers that are multithreaded? Getting the formular in CNF and substituting the variable names by numbers is easy for me. The formula in Z3 is already in CNF. The hard part for me is to use the python API to traverse and convert the formula. To traverse "And( Or(Not(A),B), Or(Not(B),C) )" to generate a string "[ [-A, B],[-B,C] ]". Thanks for your help in all your answers, also to other people! (BTW why are many links in your posts to online examples in python not working? E.g., http://rise4fun.com/Z3Py/E1s – mrsteve Oct 25 '13 at 16:25
  • Picosat is very efficient – Leonardo de Moura Oct 25 '13 at 16:29
  • There are several multithreaded SAT solvers. Example: manysat (http://www.cril.univ-artois.fr/~jabbour/manysat.htm) – Leonardo de Moura Oct 25 '13 at 16:29
  • Regarding Z3Py, we had to temporarily disable it due to security issues. See http://tomforb.es/breaking-out-of-secured-python-environments – Leonardo de Moura Oct 25 '13 at 16:30
  • Plingeling (http://fmv.jku.at/lingeling/) is another example of SAT with support for multi-threading. – Leonardo de Moura Oct 25 '13 at 16:33