CODEWITHSUNDEEP
z3smtz3py
Madalina Erascu
Madalina Erascu

Reputation: 87

Clarification SMT types; bug in variable truncation?; allowing Bool*Int

I have the following questions:

A. If I have a variable x which I declare it (case 1) to be Bool (case 2) to be Int and assert x=0 or x=1 (case 3) to be Int and assert 0<=x<=1. What happens in Z3, or more generally in SMT, in each of the cases? Is, (case 1) desired since things happen at SAT and not SMT level? Do you have some reference paper here?

B. I have the following statement in Python (for using Z3 Python API)

    tmp.append(sum([self.a[i * self.nrVM + k] * componentsRequirements[i][1] for i 
    in range(self.nrComp)]) <= self.MemProv[k])

where a is declared as a Z3 Int variable (0 or 1), componentsRequirements is a Python variable which is to be considered float, self.MemProv is declared as a Z3 Real variable.

The strange thing is that for float values for componentsRequirements, e.g 0.5, the constraint built by the solver considers it 0 and not 0.5. For example in:

    (assert (<= (to_real (+ 0 (* 0 C1_VM2)
            (* 0 C2_VM2)
            (* 2 C3_VM2)
            (* 2 C4_VM2)
            (* 3 C5_VM2)
            (* 1 C6_VM2)
            (* 0 C7_VM2)
            (* 2 C8_VM2)
            (* 1 C9_VM2)
            (* 2 C10_VM2)))
StorageProv2))

the 0 above should be actually 0.5. When changing a to a Real value then floats are considered, but this is admitted by us because of the semantics of a. I tried to use commutativity between a and componentsRequirements but with no success.

C. If I'd like to use x as type Bool and multiply it by an Int, I get, of course, an error (Bool*Real/Int not allowed), in Z3. Is there a way to overcome this problem but keeping the types of both multipliers? An example in this sense is the above (a - Bool, componentsRequirements - Real/Int): a[i * self.nrVM + k] * componentsRequirements[i][1]

Thanks

Upvotes: 2

Views: 125

Answers (2)

alias
alias

Reputation: 30418

Regarding A

Patrick gave a nice explanation for this one. In practice, you really have to try and see what happens. Different problems might exhibit different behavior due to when/how heuristics kick in. I don't think there's a general rule of thumb here. My personal preference would be to keep booleans as booleans and convert as necessary, but that's mostly from a programming/maintenance perspective, not an efficiency one.

Regarding B

Your "division" getting truncated problem is most likely the same as this: Retrieve a value in Z3Py yields unexpected result

You can either be explicit and write 1.0/2.0 etc.; or use:

 from __future__ import division

at the top of your program.

Regarding C

SMTLib is a strongly typed language; you cannot multiply by a bool. You have to convert it to a number first. Something like (* (ite b 1 0) x), where b is your boolean. Or you can write a custom function that does this for you and call that instead; something like:

(define-fun mul_bool_int ((b Bool) (i Int)) Int (ite b i 0))
(assert (= 0 (mul_bool_int false 5)))
(assert (= 5 (mul_bool_int true 5)))

Upvotes: 1

Patrick Trentin
Patrick Trentin

Reputation: 7342

I honestly can't answer for z3 specifically, but I want to state my opinion on point A).

In general, the constraint x=0 v x=1 is abstracted into t1 v t2, where t1 is x=0 and t2 is x=1, at the SAT engine level.

Thus, the SAT engine might try to assign both t1 and t2 to true during the construction of a satisfiable truth assignment for the input formula. It is important to note that this is a contradiction in the theory of LAR, but the SAT engine is not capable of such reasoning. Therefore, the SAT engine might continue its search for a while after taking this decision.

When the LAR Solver is finally invoked, it will detect the LAR-unsatisfiability of the given (possibly partial) truth assignment. As a consequence, it (should) hand the clause not t1 or not t2 to the SAT engine as learning clause so as to block the bad assignment of values to be generated again.

If there are many of such bad assignments, it might require multiple calls to the LAR Solver so as to generate all blocking clauses that are needed to rectify the SAT truth assignment, possibly up to one for each of those bad combinations.

Upon receiving the conflict clause, the SAT engine will have to backjump to the place where it made the bad assignment and do the right decision. Obviously, not all the work done by the SAT engine since it made the bad assignment of values gets wasted: any useful clause that was learned in the meanwhile will certainly be re-used. However, this can still result in a noticeable performance hit on some formulas.

Compare all of this back-and-forth computation being wasted with simply declaring x as a Bool: now the SAT engine knows that it can only assign one of two values to it, and won't ever assign x and not x contemporarily.

In this specific situation, one might mitigate this problem by providing the necessary blocking clauses right into the input formula. However, it is not trivial to conclude that this is always the best practice: explicitly listing all known blocking clauses might result in an explosion of the formula size in some situations, and into an even worse degradation of performance in practice. The best advice is to try different approaches and perform an experimental evaluation before settling for any particular encoding of a problem.

Disclaimer: it is possible that some SMT solvers are smarter than others, and automatically generate appropriate blocking clauses for 0/1 variables upon parsing the formula or avoid this situation altogether through other means (i.e. afaik, Model-Based SMT solvers shouldn't incur in the same problem)

Upvotes: 0

Related Questions