Issues with utilizing Z3 for MAX-SAT

Question

I am interested in MAX-SAT and was hoping Z3 would have this as a built-in feature. Are there any plans to do this in the near future?

In the absence of the above, I have tried using the example maxsat application from the command line. Unfortunately, whenever I do exec.sh "filename.z3", I always get the following response: "checking whether hard constraints are satisfiable...result: 0". What am I doing wrong? I assure you that this response appears to be quite independent of the actual contents of the file.

Finally, the comments in the maxsat example do not clearly specify how to mark constraints as hard or soft. A hard constraint is supposed to be a formula preceded by :formula, and a soft constraint a formula preceded by :assumption. So, to mark "(assert (> x 0))" as soft, where exactly do we put the ":assumption"? (I am have read the query about hard and soft constraints, but the question/response seemed to be more in the context of finding unsatisfiable cores, as opposed to "maximum satisfiable cores" of unsatisfiable formulas.)

Leonardo de Moura Leonardo de Moura · Accepted Answer · 2012-05-22T01:07:09

The MaxSAT example in the Z3 distribution demonstrates how to implement two MaxSAT algorithms using the Z3 API. The example still uses the old (deprecated) API for asserting constraints, but it can be easily modified to use the new solver API. The example application reads a SMT 1.0 file. However, the MaxSAT functions can be used on formulas created using the C API. The script assumes that :assumption fields are soft constraints and :formula is a hard one. Here is a small example, where (> x 0), (> y 0), (< x y) and (> x (- y 1)) are soft constraints, and (> (+ x y) 0) and (< (- x y) 100) are hard ones. The example application returns 3. That is, at most three of the soft constraints can be satisfied.

(benchmark ex
  :extrafuns ((x Int))
  :extrafuns ((y Int))
  ;; Soft Constraints
  :assumption (> x 0)
  :assumption (> y 0)
  :assumption (< x y)
  :assumption (> x (- y 1))
  :formula 
  (and 
  ;; Hard Constraints
  (> (+ x y) 0)
  (< (- x y) 100)
))

That being said, we do not have plans to support MaxSAT directly in the Z3 API. In future versions, we may port the MaxSAT example to other APIs (.NET, Python and C++).

Issues with utilizing Z3 for MAX-SAT

1 Answers