3

I have a SMT application (built on Haskell SBV library), which solves some complex equation against single s variable in Real logic using Z3. Finding solution takes about 30 seconds in my case.

Trying to speed things up, I added additional constraint s < 40000, as I have some estimation of solution. I was thinking that such constraint would shrink the search space and make solver return the result faster. However, this only made it slower (it didn't even finished in 10 minutes, actually).

The question is: can it be assumed that additional constraints always slows down/speeds up solution process, or there are no general rules and it always depends on circumstances?

I'm worried that even my 30-seconds algorithm may contain some extra constraint that isn't necessarily needed, but just slows the process.

arrowd
  • 33,231
  • 8
  • 79
  • 110
  • 1
    In general, @Levent Erkok is correct: heuristics/etc. employed by SMT solvers make their performance seldom predictable. However, there is always the possibility that the exhibited behavior is not a fluke but something consistently true "in general" with respect to the solver used or the problem/encoding being considered. Perhaps it is worth experimenting with it a bit, trying different instances of the problem, different bounds and different solvers. If there is some consistent, measurable, pattern, then maybe it's worth a deeper investigation and getting more attention from the community. – Patrick Trentin Feb 14 '19 at 00:10

1 Answers1

3

I don't think you can make any general assumptions about this. It may or may not impact solving time, assuming sat/unsat status doesn't change.

Equalities usually help (as they propagate freely), but for anything else, it's anybody's guess. Also, different solvers can exhibit differing behavior for the same addition.

One way to think about this is that the underlying DPLL(T) algorithm is essentially a very smart glorified search algorithm. It keeps producing "learned lemmas" with the hope that it will find a contradiction with a previously known fact. The new "constraint" you add might cause it to generate a ton of correct but irrelevant lemmas that makes it go down the deep-end with no useful result. (Quantified formulae are usually like this: You can instantiate them in a million different ways; but unless you find the "correct" instantiation, all they do is end up polluting your search space.)

At least that's been my experience!

alias
  • 28,120
  • 2
  • 23
  • 40