CODEWITHSUNDEEP
z3boolean-logicsat
Jes
Jes

Reputation: 2694

Arithmetic operation on Z3 bool variable

I have a bunch of boolean variables in Z3, say ai, bj, and ck, to formulate my SAT problem. However, in my problem, there are three arithmetic constraints to be considered:

a1 + a2 + a3 + ... + an = 1
b1 + b2 + b3 + ... + bn = 0
c1 + c2 + c3 + ... + cn <= 1

How can I formulate these three arithmetic constraints using Z3 API without changing the variable type (i.e., all boolean by default)?

Upvotes: 1

Views: 1375

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 8359

You can embed Booleans into an if-expression, e.g., you can write

  if(a1,1,0) + if(a2,1,2) + ...

As a somewhat special purpose feature, it is also possible to enter cardinality constraints directly using built-in cardinality operators at this point from the C, .NET, and Java APIs, but not python nor Ocaml. Also, the lia2pb tactic converts goals that use if-then-else expressions (as above) and converts them into Pseudo-Boolean constraints.

Upvotes: 2

Related Questions