z3py cast constraint on number satisfiable of Exists

Question

I am very new to z3/z3py.

My goal:

Suppose I have a IntVector of size 5. I have 5 Exists(...) expressions and want to store whether the exists expressiosn is true or false as 1 and 0 in the IntVector at the corresponding position. In the end, I want to set a constraint of Sum(IntVector) to a number indicating that there must be this many Exists expressions are true and the rest false. I don't care whether the Exists expressions are satisfiable or not, and the only thing I expect is whether a certain number of the Exists expressions are true.

My Problem:

I simply use a Solver and add all above assumptions to it to check the satisfiability. The above implementation takes a long time and returns "unknown". But if I check just one of the Exists expression without adding the constraint of number of true Exists expressions, I will get sat or unsat in a short time. If I check all Exists expressions together without adding the constraint of number of true Exists expressions, I will get unsat (because some the Exists expressions are essentially unsat). I feel tactics and subgoals might solve my problem. But I don't yet have enough knowledge about them.

I hope my problem above makes sense. Could anyone give me some pointers here?

Hi, Sergey. Thanks for your reply. Unfortunately, my code is under a non-disclosure agreement so I probably should not post it. But I figure out that the constraint Not(Exists(...)) always return "unknown", which might caused the problem. I am now using an alternative method to avoid writing Not(Exists(...)). — Zhongjun 'Mark' Jin

Nikolaj Bjorner Nikolaj Bjorner · Accepted Answer · 2015-06-13T01:04:57

Maybe you can view this as a max-sat problem. I recently added optimization features to Z3, which allows you to pose soft constraints. Furthermore solving satisfiabiltiy of Exists(x1, Fml(x1)) amounts to solving satisfiability of Fml(x1), where x1 is a free constant. So it sounds like the existential closure is an overkill.

Example:

 (define-fun f1 ((x Int)) Bool < definition of formula f1 >)
 (define-fun f2 ((x Int)) Bool < definition of formula f2 >)
 (define-fun f3 ((x Int)) Bool < definition of formula f3 >)
 (declare-const x1 Int)
 (declare-const x2 Int)
 (declare-const x3 Int)

 (assert-soft (f1 x1))
 (assert-soft (f2 x2))
 (assert-soft (f3 x3))

 (check-sat)

The result will maximize the number of satisfied soft constraints. Part of the output is the number of violated soft constraints.

z3py cast constraint on number satisfiable of Exists

1 Answers