strange performance for (= x y) vs. (= y x)

[DvonHolten]

attached are 3 files which differ only in the order of some function arguments: one is the original, with 'unordered' arguments, one with lexically ascending and the other one with lexically descending arguments. The table show the runtimes of each version with Z3 4.7.1 and the nightly build of 26. august.
The first two parameters go into an (= expression in the function isNeighbor, which looks like this (at line 140):

(define-fun isNeighbor ( (v1 Int) (v2 Int) (p1 Int) (p2 Int) ) Bool
     (and 
         (= v1 v2)              ; row/row is equal          
         (dist-Eql-1 p1 p2)     ; col/col have distance 1
     )
)`

The order of the last two parameters is required as shown. In an attempt to tidy up the code i arranged the first two arguments - to find a dramatic, unexplainable difference in the runtime, shown in seconds.

               Z3 v4.7.1    v4.8.0 (26 Aug)
v123a.smt          74        90
v124a.smt         251       166
v124b.smt         544        97

What is going on here? Does it mean, problems (of the right kind) have a considerable 'silent performance reserve' which can be leveraged by just reordering variables?

Here is an original, unordered block (at line 4317 in v123a.smt):

(assert` (= cv-2073-27-68-15 
  (or 
     (and i-68-rot-2 i-27-rot-2    (isNeighbor  i-27-col i-68-col i-27-row i-68-row    ) )
     (and i-68-rot-3 i-27-rot-3    (isNeighbor  i-68-row i-27-row i-68-col i-27-col    ) )
     (and i-68-rot-0 i-27-rot-0    (isNeighbor  i-68-col i-27-col i-68-row i-27-row    ) )
     (and i-68-rot-1 i-27-rot-1    (isNeighbor  i-27-row i-68-row i-27-col i-68-col    ) )
 )  ; close or 2                                ^^^^^^^^^^^^^^^^^^
))

Here is a code-block with first two arguments ordered descending (in file v124a.smt):

(assert (= cv-2073-27-68-15 
  (or 
     (and i-68-rot-2 i-27-rot-2    (isNeighbor  i-68-col i-27-col i-27-row i-68-row    ) )
     (and i-68-rot-3 i-27-rot-3    (isNeighbor  i-68-row i-27-row i-68-col i-27-col    ) )
     (and i-68-rot-0 i-27-rot-0    (isNeighbor  i-68-col i-27-col i-68-row i-27-row    ) )
     (and i-68-rot-1 i-27-rot-1    (isNeighbor  i-68-row i-27-row i-27-col i-68-col    ) )
 )  ; close or 2                                ^^^^^^^^^^^^^^^^^^
))

Here is a code-block with first two arguments ordered ascending (in file v124b.smt):

(assert (= cv-2073-27-68-15 
  (or 
     (and i-68-rot-2 i-27-rot-2    (isNeighbor  i-27-col i-68-col i-27-row i-68-row    )  )
     (and i-68-rot-3 i-27-rot-3    (isNeighbor  i-27-row i-68-row i-68-col i-27-col    )  )
     (and i-68-rot-0 i-27-rot-0    (isNeighbor  i-27-col i-68-col i-68-row i-27-row    )  )
     (and i-68-rot-1 i-27-rot-1    (isNeighbor  i-27-row i-68-row i-27-col i-68-col    )  )
 )  ; close or 2                                ^^^^^^^^^^^^^^^^^^
))

z310x10H7C3v123a.smt.txt
z310x10H7C3v124b.smt.txt
z310x10H7C3v124a.smt.txt

[NikolajBjorner]

The problem is SAT. If the solver is lucky it can find a solution immediately. There is generally quite some fluctuation of time taken for SAT problems (often more than the fluctuation observed on "common" examples that are unsat). You can obtain other fluctuations just by tinkering with the value of smt.random_seed.
For fun you can try the "psmt" tactic and control parameters under the "parallel" name space (run z3 -pm:parallel for options).
It is possible that your problems will perform better when formulated using only Booleans and bit-vectors, in this case the SAT solver would be invoked by default. (you will see lines that start with "sat" instead of lines that start with "smt" if you run in verbose mode). The "sat" mode supports additional multi-threading that evens out performance: you can run multiple instances of the sat solver in parallel on the same problem. It tends to reduce average time. Inspect -pm:sat for options.

[DvonHolten]

thanks for response . i have modelled with SAT before and arrived at SMT recently. Is Z3 SAT-solving competitive with plingeling ? I'll stick with mixed integer-boolean modelling until i run out of ideas.
I found that parallel-thing in the release-note of version 4.8 - and i found a number of posts here and in stackoverflow about parallels - i even found the 2009 paper of your team describing the architecture of parallel Z3 .
But nobody gives an example how to configure it ! whatever i try gives either error-messages or exact the same numbers and times as in normal mode.
Can you give the precise command to enable parallel-mode ??

[NikolajBjorner]

The 2009 paper is unrelated. That code is long gone.
There is a separate GitHub issue asking for examples of using parallel mode, #1898, where I give an example. I will collect comments on parallel mode there.
See also http://theory.stanford.edu/~nikolaj/programmingz3.html for
the sections on Parallel Z3 and Section 6.2.2. on Co-processing (you can spawn multiple parallel solvers that share learned clauses).