CODEWITHSUNDEEP
z3smtz3pybipartitesat
Shriphani Palakodety
Shriphani Palakodety

Reputation: 41

Confused about a simple SAT matching problem using Z3

I am trying to solve a simple matching problem using Z3 which it claims is unsat. I have set this up the following way:

finally, I want to maximize the number of matchings. So I have:

I was able to whip this up quite quickly using z3-rs in Rust (not sure if that makes a difference). And this is the solver state before I run check on it:

Solver: (declare-fun p_0_0 () Bool)
(declare-fun p_1_0 () Bool)
(declare-fun k!0 () Int)
(declare-fun k!1 () Int)
(assert (=> p_0_0 true))
(assert (=> p_1_0 true))
(assert ((_ at-most 1) p_0_0))
(assert ((_ at-most 1) p_1_0))
(assert ((_ at-most 1) p_0_0 p_1_0))
(maximize (+ (ite p_1_0 k!1 k!0) (ite p_0_0 k!1 k!0)))
(check-sat)

Z3 claims this is Unsat and I am quite stumped. I don't see why p_0_0 = T, p_1_0 = F doesn't satisfy this formula.

Thank you very much for the help.

Upvotes: 0

Views: 223

Answers (1)

alias
alias

Reputation: 30418

I can't replicate this. When I run your program, z3 prints: (after adding (get-model) at the end)

sat
(
  (define-fun p_0_0 () Bool
    true)
  (define-fun p_1_0 () Bool
    false)
  (define-fun k!1 () Int
    0)
  (define-fun k!0 () Int
    (- 1))
)

which matches your expectations.

Couple of things to make sure:

  • Is your z3 version "new" enough? 4.11.3 is the latest master I think
  • You mentioned you use it from Rust. Perhaps you didn't use the rust-API correctly? Or, maybe Rust interface has a bug.

I'd start by running it manually on your machine using the SMTLib script you've given. If you get SAT (which you should!), perhaps ask at the Rust forum as the bug is likely either in your Rust program or the Rust bindings itself. If you get UNSAT, try upgrading your z3 installation and possibly recompile the Rust bindings if that's relevant. (I'm not familiar with the Rust bindings to say if it needs a recompile or not if you upgrade your z3. It could be either way.)

A guess

Without seeing the details, it's hard to opine further. However, notice that you've posed this as an optimization problem; and asked z3 to maximize the addition of two uninterpreted integers. So, it's possible the Rust bindings are adding a call of the form:

(get-objectives)

at the end, to which z3 will respond:

sat
(objectives
 ((+ (ite p_1_0 k!1 k!0) (ite p_0_0 k!1 k!0)) oo)
)

That is, the objective you're maximizing is unbounded. This means there's no value for k!0 and k!1 the solver can present to you: The goal gets arbitrarily large as these get larger. It's possible the Rust interface is internally treating this as "unsat" since it cannot find the values for these constants. But that's just my guess without knowing the specifics of how the Rust bindings work.

Upvotes: 1

Related Questions