(Z3Py) Checking All Solutions for Equation

(Z3Py) checking all solutions for equation

You can do that by adding a new constraint that blocks the model returned by Z3.
For example, suppose that in the model returned by Z3 we have that x = 0 and y = 1. Then, we can block this model by adding the constraint Or(x != 0, y != 1).
The following script does the trick.
You can try it online at: http://rise4fun.com/Z3Py/4blB

Note that the following script has a couple of limitations. The input formula cannot include uninterpreted functions, arrays or uninterpreted sorts.

from z3 import *

# Return the first "M" models of formula list of formulas F 
def get_models(F, M):
    result = []
    s = Solver()
    s.add(F)
    while len(result) < M and s.check() == sat:
        m = s.model()
        result.append(m)
        # Create a new constraint the blocks the current model
        block = []
        for d in m:
            # d is a declaration
            if d.arity() > 0:
                raise Z3Exception("uninterpreted functions are not supported")
            # create a constant from declaration
            c = d()
            if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:
                raise Z3Exception("arrays and uninterpreted sorts are not supported")
            block.append(c != m[d])
        s.add(Or(block))
    return result

# Return True if F has exactly one model.
def exactly_one_model(F):
    return len(get_models(F, 2)) == 1

x, y = Ints('x y')
s = Solver()
F = [x >= 0, x <= 1, y >= 0, y <= 2, y == 2*x]
print get_models(F, 10)
print exactly_one_model(F)
print exactly_one_model([x >= 0, x <= 1, y >= 0, y <= 2, 2*y == x])

# Demonstrate unsupported features
try:
    a = Array('a', IntSort(), IntSort())
    b = Array('b', IntSort(), IntSort())
    print get_models(a==b, 10)
except Z3Exception as ex:
    print "Error: ", ex

try:
    f = Function('f', IntSort(), IntSort())
    print get_models(f(x) == x, 10)
except Z3Exception as ex:
    print "Error: ", ex

Trying to find all solutions to a boolean formula using Z3 in python

The typical way to code such problems is as follows:

from z3 import *

a, b, c = Bools('a b c')
s = Solver()
s.add(Or([a, b, c]))

res = s.check()
while (res == sat):
  m = s.model()
  print(m)
  block = []
  for var in m:
      block.append(var() != m[var])
  s.add(Or(block))
  res = s.check()

This prints:

[b = True, a = False, c = False]
[a = True]
[c = True, a = False]

You'll notice that not all models are "complete." This is because z3 will typically "stop" assigning variables once it decides the problem is sat, as the other variables are irrelevant.

I suppose your confusion is that there should be 7 models to your problem: Aside from the all-False assignment, you should have a model. If you want to get the values of all your variables in this way, then you should explicitly query for them, like this:

from z3 import *

a, b, c = Bools('a b c')
s = Solver()
s.add(Or([a, b, c]))

myvars = [a, b, c]

res = s.check()
while (res == sat):
  m = s.model()
  block = []
  for var in myvars:
      v = m.evaluate(var, model_completion=True)
      print("%s = %s " % (var, v)),
      block.append(var != v)
  s.add(Or(block))
  print("\n")
  res = s.check()

This prints:

a = False  b = True  c = False

a = True  b = False  c = False

a = True  b = True  c = False

a = True  b = True  c = True

a = True  b = False  c = True

a = False  b = False  c = True

a = False  b = True  c = True

And there are exactly 7 models as you would've expected.

Note the model_completion parameter. This is a common pitfall for newcomers as there isn't a "out-of-the-box" method in z3 for getting all possible assignments, so you have to be careful coding it yourself like above. The reason why there isn't such a function is that it's really hard to implement it in general: Think about how it should work if your variables were functions, arrays, user-defined data-types, etc. as opposed to simple booleans. It can get really tricky to implement a generic all-sat function with all these possibilities handled correctly and efficiently. So, it's left to the user, as most of the time you only care about a specific notion of all-sat that's typically not hard to code once you learn the basic idioms.

Getting all solutions of a boolean expression in Z3Py never ends

I would advice you to try writing your loop like this instead:

from z3 import *

a = Bool('a')
b = Bool('b')

f1 = Or(a,b)
s = Solver()
s.add(f1)

while s.check() == sat:

    m = s.model()

    v_a = m.eval(a, model_completion=True)
    v_b = m.eval(b, model_completion=True)

    print("Model:")
    print("a := " + str(v_a))
    print("b := " + str(v_b))

    bc = Or(a != v_a, b != v_b)
    s.add(bc)

The output is:

Model:
a := True
b := False
Model:
a := False
b := True
Model:
a := True
b := True

The argument model_completion=True is necessary because otherwise m.eval(x) behaves like the identity relation for any x Boolean variable with a don't care value in the current model m and it returns x as a result instead of True/False. (See related Q/A)

---

NOTE: since z3 kindly marks don't care Boolean variables, an alternative option would be to write your own model generator that auto-completes any partial model. This would reduce the number of calls to s.check(). The performance impact of this implementation is hard to gauge, but it might be slightly faster.

Find all optimal solutions with Optimize() from z3py

It's not quite clear what you mean by "optimal" in this context. It appears you allow the soft-constraints to be violated, but at least one of them must hold? (After all, ([x=True, y=True] is a valid solution, violating both your soft-constraints; which you did allow by explicitly calling all_smt.)

Assuming you are indeed looking for solutions that satisfy at least one of the soft-constraints, you should explicitly code that up and assert as a separate predicate. The easiest way to do this would be to use tracker variables:

from z3 import *

def all_smt(s, initial_terms):
    def block_term(s, m, t):
        s.add(t != m.eval(t, model_completion=True))
    def fix_term(s, m, t):
        s.add(t == m.eval(t, model_completion=True))
    def all_smt_rec(terms):
        if sat == s.check():
           m = s.model()
           yield m
           for i in range(len(terms)):
               s.push()
               block_term(s, m, terms[i])
               for j in range(i):
                   fix_term(s, m, terms[j])
               yield from all_smt_rec(terms[i:])
               s.pop()
    yield from all_smt_rec(list(initial_terms))

x, y = Bools('x y')
s = Optimize()

s.add(Or(x,y))

p1, p2 = Bools('p1 p2')
s.add(Implies(p1, Not(x)))
s.add(Implies(p2, Not(y)))

asserted = If(p1, 1, 0) + If(p2, 1, 0)
s.add(asserted >= 1)
s.minimize(asserted)

print([[(x, m[x]), (y, m[y])] for m in all_smt(s, [x,y])])

Here, we use p1 and p2 to track whether the soft-constraints are asserted, and we minimize the number of soft-constraints via the variable asserted yet requiring it should at least be 1. When run, the above prints:

[[(x, True), (y, False)], [(x, False), (y, True)]]

which seems to be what you wanted to achieve in the first place.

What is the most efficient way of checking N-way equation equivalence in Z3?

As with anything performance related, the answer is "it depends." Before delving into options, though, note that z3 supports Distinct, which can check whether any number of expressions are all different: https://z3prover.github.io/api/html/namespacez3py.html#a9eae89dd394c71948e36b5b01a7f3cd0

Though of course, you've a more complicated query here. I think the following two algorithms are your options:

Explicit pairwise checks

Depending on your constraints, the simplest thing to do might be to call the solver multiple times, as you alluded to. To start with, use Distinct and make a call to see if its negation is satisfiable. (i.e., check if some of these expressions can be made equal.) If the answer comes unsat, you know you can't make any equal. Otherwise, go with your loop as before till you hit the pair that can be made equal to each other.

Doing multiple checks together

You can also solve your problem using a modified algorithm, though with more complicated constraints, and hopefully faster.

To do so, create Nx(N-1)/2 booleans, one for each pair, which is equal to that pair not being equivalent. To illustrate, let's say you have the expressions A, B, and C. Create:

• X0 = A != B
• X1 = A != C
• X2 = B != C

Now loop:

• Ask if X0 || X1 || X2 is satisfiable.
• If the solver comes back unsat, then all of A, B, and C are equivalent. You're done.
• If the solver comes back sat, then at least one of the disjuncts X0, X1 or X2 is true. Use the model the solver gives you to determine which ones are false, and continue with those until you get unsat.

Here's a simple concrete example. Let's say the expressions are {1, 1, 2}:

• Ask if 1 != 1 || 1 != 2 || 1 != 2 is sat.
• It'll be sat. In the model, you'll have at least one of these disjuncts true, and it won't be the first one! In this case the last two. Drop them from your list, leaving you with 1 != 1.
• Ask again if 1 != 1 is satisfiable. The answer will be unsat and you're done.

In the worst case you'll make Nx(N-1)/2 calls to the solver, if it happens that none of them can be made equivalent with you eliminating one at a time. This is where the first call to Not (Distinct(A, B, C, ...)) is important; i.e., you will start knowing that some pair is equivalent; hopefully iterating faster.

Summary

My initial hunch is that the second algorithm above will be more performant; though it really depends on what your expressions really look like. I suggest some experimentation to find out what works the best in your particular case.

A Python solution

Here's the algorithm coded:

from z3 import *

exprs = [IntVal(i) for i in [1, 2, 3, 4, 3, 2, 10, 10, 1]]

s = Solver()

bools = []
for i in range(len(exprs) - 1):
  for j in range(i+1, len(exprs)):
    b = Bool(f'eq_{i}_{j}')
    bools.append(b)
    s.add(b == (exprs[i] != exprs[j]))

# First check if they're all distinct
s.push()
s.add(Not(Distinct(*exprs)))
if(s.check()== unsat):
    quit("They're all distinct")
s.pop()

while True:
    # Be defensive, bools should not ever become empty here.
    if not bools:
        quit("This shouldn't have happened! Something is wrong.")

    if s.check(Or(*bools)) == unsat:
        print("Equivalent expressions:")
        for b in bools:
          print(f'   {b}')
        quit('Done')
    else:
        # Use the model to keep bools that are false:
        m = s.model()
        bools = [b for b in bools if not(m.evaluate(b, model_completion=True))]

This prints:

Equivalent expressions:
   eq_0_8
   eq_1_5
   eq_2_4
   eq_6_7
Done

which looks correct to me! Note that this should work correctly even if you have 3 (or more) items that are equivalent; of course you'll see the output one-pair at a time. So, some post-processing might be needed to clean that up, depending on the needs of the upstream algorithm.

Note that I only tested this for a few test values; there might be corner case gotchas. Please do a more thorough test and report if there're any bugs!

(z3py) Generate all solutions for a 2D list using all_smt

initial_terms is supposed to be a simple list of terms that you want to not "duplicate" in the models. If you have a 2d (or n-d for whatever n), simply flatten it before you pass it to all_smt.

An easy way to flatten a 2-D list would be:

>>> import itertools
>>> list(itertools.chain(*[[1,2,3],[4,5,6],[7,8,9]]))
[1, 2, 3, 4, 5, 6, 7, 8, 9]

If you have higher-dimensions, you can write a similar function to flatten them down accordingly.

---

Related Topics