9
$\begingroup$

SMT solvers such as Z3 or Boolector use a complex set of heuristics to solve problems. However, this also makes predicting the performance of such a solver for a given problem very hard. My question is thus:

Question

Is there a way to understand or gain insights into the performance of a SMT solver for a specific in the theory of quantifier-free bitvectors (QFBV)?

This also includes any visualization tools that would help to understand where the solver is "stuck" / does not make progress.

Applications

  • Understand in advance how different encodings of the same problem affect solver performance (the state of the art here can't be "just try a few different encodings and hope one is fast enough", right?)

  • If a given problem is not solveable by an SMT solver due to time constraints, find a way to express the problem differently so that it can be solved.

  • Avoid wasting time on domain-specific problem simplifications that won't affect solver performance at all or even negatively affect solver performance.

Existing research

I tried to find research on this topic, but I have not been able to find much. I do not have much experience in the field of SAT/SMT solvers yet, so apologies if I have missed something.

  • SATzilla: predicts best performing solver based on features extracted from the problem using machine-learning techniques.

    This applies only with SAT instead of SMT, and does not explain the reasons for solvers performance.

  • Z3 axiom profiler A visualization of Z3 instantiation graph and analysis of matching loops

    Looks like this focuses only on the quantified theories.

Improve this question
$\endgroup$

1 Answer 1

Reset to default
3
$\begingroup$

The short answer is no, we don't understand it. The long answer is yes, we have some bounds, but those bounds aren't very helpful. It's quite clear that the worst-case running time is exponential. That's not very helpful, because we know that in some/many practical situations, it seems to run fairly rapidly -- and we don't really know why.

We don't know why that is true for SAT solvers, let alone for QFBV. Understanding why QFBV solvers are often fast seems at least as hard as understanding why SAT solvers are often fast, which is already beyond our current level of understanding. If you search more on this site you can find a summary of current attempts to understand the latter topic.

Improve this answer
$\endgroup$
1
  • $\begingroup$ thanks for your answer! i had already though that may be the case. Do you know if there is any research that doesn't try to find general rules, but instead visualize the reason for slow performance of a sat/smt solver (or in another way help the user understand what part of the problem is giving and SMT solver touble) $\endgroup$
    – bennofs
    Sep 7, 2017 at 21:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.