Max-SMT problem

[FoxMakarov]

Hello! I have some questions when I tried to solve a max-smt problem.

We can describe a max-smt problem with a hard constraint and some soft constraint. In z3 Guide, it teaches me to describe this kind of problem like :

(declare-const x Int)
(declare-const y Int)
(define-fun a1 () Bool (> x 0))
(define-fun a2 () Bool (< x y))
(define-fun a3 () Bool (<= (+ y x) 0))
(assert (= a3 a1))
(assert (or a3 a2))
(assert-soft a3         :weight 3)
(assert-soft (not a3)   :weight 5) 
(assert-soft (not a1)   :weight 10)
(assert-soft (not a2)   :weight 3)
(check-sat)
(get-model)
(get-objectives)
(eval a1)
(eval a2)
(eval a3)

and its result is a1: false, a2: true, a3:false. We can know that it satisfy the target computing max weight of four soft constraints.

I want to finish a program like this. But I learn the z3 rust Guide, I just find the function check_assumptions. Its desctibtion is "Check whether the assertions in the given solver and optional assumptions are consistent or not.", I think the assertion is hard-constraint and assumptions are soft-constraints. So I use the function like this:

solver.assert(&query); //query is hard-constraint, must satisfy
let result = solver.check_assumptions(assumption); //assumption is soft-constraint array, [10<=2, 10>=2]

run result : z3::SatResult::Unsat

I don't know why.
Don’t soft constraints refer to constraints that can be satisfied or not? As long as the hard constraints are satisfied, the solution can be successfully solved. When just the code "soler.assert(&query); solver.check();" meaning only hard constraints, the result can be obtained.

Is there something wrong with my encoding of the max-smt problem? This function does not meet my needs? I'm really looking forward to your help!

[Pat-Lafon]

Here "optional assumptions" means that the list can be empty(you don't need to provide any assumptions), not that the constraints provided are soft. See this post for a more official description/comparison with the normal solver.check(): Z3Prover/z3#1152. You are looking for https://docs.rs/z3/latest/z3/struct.Optimize.html instead.

[FoxMakarov]

Thank you so much!

I try to use Optimize to meet my needs. I used these three functions Optimize::assert_soft()
Optimize::maximize()
Optimize::minimize()
But the result is confused.

        let zero = Int::from_i64(self.context, 0);
        let one = Int::from_i64(self.context, 1);
        let t = Int::fresh_const(self.context, "t");
        let value_of_t = Bool::or(self.context, &[&t._eq(&zero),&t._eq(&one)]);  //t=0 or t = 1

        let query = z3::ast::Bool::<'_>::and(self.context, &[&query, &value_of_t]); 
        solver.assert(&query);  //query is hard-constraini=t

        let t_ge_0 = Int::ge(&t, &zero);//t>=0
        let t_ge_1 = Int::ge(&t, &one);//t>=1
        
        //method1 result t = 1
        solver.assert_soft(&t_ge_0, 1, Some(z3::Symbol::Int(0)));
        solver.assert_soft(&t_ge_1, 1, Some(z3::Symbol::Int(0)));
        solver.check(&[]);

       //method2 result t = 0
        solver.maximize(&Bool::or(self.context, &[&t_ge_0, &t_ge_1]));
        solver.check(&[]);

        //method3 result t = 0
        solver.minimize(&Bool::or(self.context, &[&t_ge_0, &t_ge_1]));
        solver.check(&[]);

If the value of "t" is 1, then both the formulas t>=0 and t>=1 can be satisfied. In my opinion, both assert_soft and maximize should get the result of t = 1, because this can satisfy more formulas, while minimize should get t = 0, so that the least formula can be satisfied. But the running result is that maximize and minimize get t = 0.

So "assert_soft" can get the result with the highest sum of the added soft constraint weights, but don’t the functions of "maximize" and "minimize" mean to get the maximum or minimum sum of weights?

Is there any problem with my understanding of these three functions?

[Pat-Lafon]

When you are providing code, please keep it to a minimal and executable example. I don't know what self.context is and let query = z3::ast::Bool::<'_>::and(self.context, &[&query, &value_of_t]); doesn't seem to be a valid given what you have provided.

Just solver.check(&[]); is what you are looking for. Maximize and minimize are for providing a cost function that you want to maximize or minimize... imagine you had 2 integers x and y, you might want to maximize or minimize their sum, x + y and would provide that as an ast. It's fair that the documentation is not clear on this so maybe you can submit a pr with a doctest or open a pr with Z3 itself for better documentation(Since the rust bindings usually just parrot the descriptions that the main z3 project uses).

[Pat-Lafon]

There is a test called test_solve_simple_semver_example that has an example usage of maximize, if that can provide more clarity.

[FoxMakarov]

Thank you for pointing out my question. I think I understand what you mean. thanks for your help！