Z3py: Convert a Z3 formula to clauses used by picosat

Question

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)

Answer 1

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

• Z3 and DIMACS output

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

• Substituting function symbols in z3 formulas
• Is there a way of querying or accessing the structure of a Z3 expression via the API

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

• Hashing expressions in Z3Python