Z3 solver returning unsat when formula should be satisfiable

Question

I got a 'simple' formula that the Z3 solver (python interface) seems unable to handle. It is running for quite some time (30 minutes) and then returning unkown even though I can find a satisfying assignment by hand in under a minute. This is the formula:

[Or(<uc 1.0> == 0, <uc 1.0> == 1),
 Or(<uc 1.1> == 0, <uc 1.1> == 1),
 Or(<uc 1.2> == 0, <uc 1.2> == 1),
 <uc 1.0> + <uc 1.1> + <uc 1.2> == 1,
 Or(<uc 0.0> == 0, <uc 0.0> == 1),
 Or(<uc 0.1> == 0, <uc 0.1> == 1),
 Or(<uc 0.2> == 0, <uc 0.2> == 1),
 <uc 0.0> + <uc 0.1> + <uc 0.2> == 1,
 Or(<uc 2.0> == 0, <uc 2.0> == 1),
 Or(<uc 2.1> == 0, <uc 2.1> == 1),
 Or(<uc 2.2> == 0, <uc 2.2> == 1),
 <uc 2.0> + <uc 2.1> + <uc 2.2> == 1,
 ForAll(c,
        Or(c > 1000,
           Or(c < -1000,
              ForAll(b,
                     Or(b > 1000,
                        Or(b < -1000,
                           ForAll(a,
                                  Or(a > 1000,
                                     Or(a < -1000,
                                        And(And(And(True,
                                        a ==
                                        <uc 0.0>*b +
                                        <uc 0.1>*c +
                                        <uc 0.2>*a),
                                        b ==
                                        <uc 1.0>*b +
                                        <uc 1.1>*c +
                                        <uc 1.2>*a),
                                        c ==
                                        <uc 2.0>*b +
                                        <uc 2.1>*c +
                                        <uc 2.2>*a))))))))))]

It may look a bit scary but let me walk you through it. < uc i.j> are all integer variables. I first specify that they should be either 0 or 1 and then I'm introducing the constraint that exactly one of them should be 1 and the others need to be 0 (using the sum).

In the second part you can ignore all the Or's which bascially just limit my search space for each variable to [-1000, 1000]. I then have the inner most constraints which should imply: < uc 0.2> = 1 < uc 1.0> = 1 < uc 2.1> = 1 and all other = 0. That's all. I'm pretty sure the solver should be able to solve this but no luck. I can change the sum constraint to something like Or(< uc 1.0>,< uc 1.1>,< uc 1.2>) which, funny enough, solves my problem in this case (the solver returns the correct assignment in seconds) but in general, this is obviously, not equivalent to what I want to have.

Questions:

• Is there something like a bit, which I could use instead of Integers?
• Some recommended way to express the fact that exactly one argument is 1?
• Some other way to make this solvable without changing the second part of the formula.

Thank you very much!

// Edit: After playing around with a few options I 'solved' it by placing the side conditions after the ForAll condition (just swapping the two lines of code). This shouldn't make a difference at all but now he is finding the correct assignment in 0.5 seconds - what? I also tried the example with 4 variables (a,b,c,d) instead (a,b,c) but then again it runs for hours... Any help? Also chaning the sum with a length And/Or did not work.

Answer 1

so I couldn't get rid of the multiplications without restructuring the whole approach so what I did instead was moving the block with all the conditions (uc=1 or uc=1 and sum = 1) below the forAll block. This worked in most cases but there were still a few tests where it would run for hours with no result. What finally did it for me was to group the forAll statements together instead of spacing them out. So instead of:

ForAll(c,
        Or(c > 1000,
           Or(c < -1000,
              ForAll(b,
                     Or(b > 1000,
                        Or(b < -1000...

I would get something like this

ForAll(c,
   ForAll(b,
        Or(c > 1000,
           Or(c < -1000,
              Or(b > 1000,
                 Or(b < -1000...

This finally solved the problem and the solver was now able to deal with all test cases. I'm a bit disappointed that it took so much try and error to get it right but at least I can solve my formulas now. Thank you!

Answer 2

I tried your example using Booleans instead of the integers for the 0-1 variables. However, this does not help too well. As it currently stands, the quantifier instantiation mechanisms could be improved to handle instances like these.