Clash Royale CLAN TAG#URR8PPP

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

1 Answer
1

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.

x=0 v x=1

t1 v t2

t1

x=0

t2

x=1

SAT

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.

SAT

t1

t2

true

LAR

SAT

SAT

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.

LAR

not t1 or not t2

SAT

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.

LAR

SAT

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.

SAT

SAT

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.

x

SAT

x

not x

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)

SMT

0/1

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.