0

I'm attempting to get Z3 to find all possible permutations of a sequence of fixed size that satisfy some constraints. However, I've run into a timeout error with the code I've developed so far:

(set-option :produce-unsat-cores true)
(set-option :produce-models true)

; --------------- Basic Definitions -------------------
(declare-datatypes () ((Obj A B C)))

; --------------- Predicates -------------------------------

(define-sort MyList () (Seq Obj))

(define-fun in_list ((o Obj) (l MyList)) Bool (seq.contains l (seq.unit o)))

(define-fun permutation ((l1 MyList) (l2 MyList)) Bool
                    (forall ((o Obj)) (= (in_list o l1) (in_list o l2))))


; Two difference permutations of the same list
(declare-const l0 MyList)
(declare-const l1 MyList)

(assert (= 2 (seq.len l0)))
(assert (= 2 (seq.len l1)))
(assert (not (= l1 l0)))
(assert (permutation l0 l1))

; --------------- Verify -------------------
(check-sat)
(get-model)

It seems like this should be a pretty trivial solve (even a brute force should take milliseconds), so I'm pretty baffled what is causing the timeout. Any help?

Kleptine
  • 5,089
  • 16
  • 58
  • 81

1 Answers1

1

You're running into limits of what Z3 can do when quantifiers are present.

You might want to look at this question: Defining a Theory of Sets with Z3/SMT-LIB2

In this case, the question is about general set operations, but I think you'll find the answers to apply to your case as well. (In short, disable MBQI, and see if you can use functions instead of sequences.)

alias
  • 28,120
  • 2
  • 23
  • 40
  • Just curious, do you know if Z3 is currently the state of the art, in terms of available solvers? Is this the sort of thing that you think will improve with time, or might it be more fundamental of an issue? – Kleptine Jun 23 '18 at 16:42
  • 1
    Solvers improve all the time. If your interest is in quantifiers and sequences, then Z3 and CVC4 are probably the best choices for the time being. But keep in mind that anytime quantifiers are present you'll have to help the solver quite a bit. (In terms of providing matching patterns.) Also, any proof that requires induction will be mostly beyond reach. For reasoning about general data-structures and induction, theorem provers (Isabelle, HOL, Coq, Lean) are the best options these days. (This is all my subjective opinion of course, so please take it with a grain of salt.) – alias Jun 23 '18 at 17:30