Search code examples
z3smtpartial-ordering

Which encodings are preferable to use Z3 to solve a partial order theory?

I'm considering diverse ways of encoding a partial order relation to feed it Z3.

The problem is already constrained in various ways and uses QF_ logic variants (LIA or LRA mostly).

I have additional constraints I could express that refine the solution with a partial order, in the form of, if variable ei>0 => a0 precedes ai, where ei is a variable of my problem that exists and ai variables are new, and represent "precedes" partial order constraints.

So this partial order will limit the solutions obtained in terms of ei in diverse ways.

A solution could be to use uninterpreted functions like this example : https://rise4fun.com/Z3/fZQc

; Coding a partial order precedes relation with UF
(declare-sort A)
(declare-fun pre (A A) Bool)
; non reflexive
(assert (forall ((x A)) (not (pre x x))))
; transitive
(assert (forall ((x A) (y A) (z A))
          (=> (and (pre x y) (pre y z)) 
              (pre x z)))) 
; anti symetric
(assert (forall ((x A) (y A))
          (=> (pre x y)  
              (not (pre y x)))))
; an UNSAT example
(declare-const a0 A)
(declare-const a1 A)
(declare-const a2 A)
(assert (pre a0 a1))
(assert (pre a1 a2))
(assert (pre a2 a0))
(check-sat)

This expresses exactly what I want, but this also introduces a new logic with quantifiers.

Another alternative is to plunge my elements into a concrete domain such as Real or Int : https://rise4fun.com/Z3/U0Hp

; Coding a partial order precedes relation with Real
; an UNSAT example
(declare-const a0 Real)
(declare-const a1 Real)
(declare-const a2 Real)
(assert (< a0 a1))
(assert (< a1 a2))
(assert (< a2 a0))
(check-sat)

The code is simpler and does not use quantifiers, but it forces (maybe ?) the solver to over-think, since Real have many more properties than the abstract domain A in the first version.

So which encoding should usually be preferred to encode partial orders ? Are there are additional parameters I should take into account or, maybe strategies I could configure to help solving this kind of problem ?

Solution

  • Avoid quantifiers if you can. SMT solver are just not good with them, especially in combinations of theories. If you can stick to Int or Real, great. If you can use bit-vectors, then that's even better since the logic will remain decidable even in the presence of non-linear functions.

    If your model really requires quantifiers, I'd argue that an SMT solver is simply not a good match. In that case, look at semi-automated systems like Isabelle, Coq, HOL etc.