CODEWITHSUNDEEP
z3
alias
alias

Reputation: 30428

Can soft-constraints be implemented via named expressions?

I'm wondering if it's possible to use named expressions to implement soft-constraints, without explicitly using manual "tracking" variables.

It's rather cumbersome to use manual tracking as described in the first message above, as it requires multiple calls to the solver (in fact 2^n calls might be needed in the worst case to get the largest possible set of soft-constraints satisfied when we have n soft constraints). Would it be possible to combine these two ideas to have Z3 implement soft constraints in a much simpler way? Based on the ideas from those two messages, I naively tried the following:

(set-option :produce-models true)
(set-option :produce-unsat-cores true)
(assert (! false :named absurd))
(check-sat)

I was hoping z3 would tell me sat since taking absurd to be false in a model would satisfy this contrived example; but it produced unsat instead; which is reasonable, but not as useful..

I'd appreciate any insights you might offer; or point me to some documentation on how z3 uses named expressions in more detail. (I skimmed through the manuals but didn't see them explained in detail anywhere.)

Upvotes: 0

Views: 534

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

The named expressions are part of the SMT-LIB 2.0 standard. In Z3, they are just "syntax sugar" for the approach that uses auxiliary Boolean constants.

In the SMT-LIB 2.0 standard, the named expressions are used for "tracking" assertions for commands such as (get-unsat-core) (see Section 5.1.5 of the SMT-LIB 2.0 reference manual). In your example, if we execute (get-unsat-core) after (check-sat) we get (absurd). Here is the link for the example online.

Regarding soft/hard constraints, it seems you want MaxSAT. Z3 comes with an example that uses 2 different algorithms to implement MaxSAT using the C API and auxiliary Boolean constants. The simplest one just uses the following basic idea.

  • For each soft constraint C_i, it asserts b_i implies C_i where b_i is a fresh Boolean variable.

  • An assignment where b_i is false is essentially ignoring the constraint C_i.

  • Use constraints of the form AtMostK to enforce that at most K b_i are false. Then, we can use linear search to find the maximal number of soft constraints that can be satisfied. We can also use binary search (in this case, only log N calls are needed where N is the number of soft constraints). Variations of this approach are used in many Pseudo-Boolean Solvers.

The example at examples\maxsat also contains a smarter algorithm suggested by Fu and Malik. The example also shows how to encode the constraint AtMostK.

Upvotes: 1

Related Questions