Clarification SMT types; bug in variable truncation?; allowing Bool*Int
![Creative The name of the picture](https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEgKPz5qhCkKGdpPJ0wkSm5JqlliSJoZg92-H4DuCruovhkVFuXerCphZt9wys_Gr3uwQyXObMHDwattjG5BSeCEl_LdDq1GPLct8qYyRyX4fZ9C93oW-TX7IGZLYDwqRgfFCXA4aUxkBAcS/s1600/1.jpg)
![Creative The name of the picture](https://blogger.googleusercontent.com/img/b/R29vZ2xl/AVvXsEh6VebLk98DYwS3K2nWZSCatab-q4HrSuRk91M4fQA8SHrKU_-x-lq1n780pSU_bIVLqMRv6pc3dhhh-Y2PUwBS9mM0BxvY1eM6XsM-e7Diu4z-wAoeDG0vB3-2_1U9RE8sO0lg4PHiIXbI/s400/Clash+Royale+CLAN+TAG%2523URR8PPP.png)
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.
Comments
Post a Comment