<p>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.</p>

<p>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.</p>

CC BY-SA 3.0
2017-09-07T21:15:14.883Z
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)
bennofs
CC BY-SA 3.0
2017-09-06T21:40:17.543Z
2017-09-07T22:02:07.777Z
2017-09-07T22:02:07.777Z
D.W.
<p>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:</p>

<h3>Question</h3>

<p>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)?</p>

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

<h3>Applications</h3>

<ul>
<li><p>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?)</p></li>
<li><p>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.</p></li>
<li><p>Avoid wasting time on domain-specific problem simplifications that won't affect solver performance at all or even negatively affect solver performance. </p></li>
</ul>

<h3>Existing research</h3>

<p>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.</p>

<ul>
<li><p><a href="http://www.cs.ubc.ca/labs/beta/Projects/SATzilla/SATzilla2012final.pdf" rel="noreferrer">SATzilla</a>: predicts best performing solver based on features extracted from the problem using machine-learning techniques. </p>

<p>This applies only with SAT instead of SMT, and does not explain the reasons for solvers performance.</p></li>
<li><p><a href="https://bitbucket.org/viperproject/axiom-profiler" rel="noreferrer">Z3 axiom profiler</a> A visualization of Z3 instantiation graph and analysis of matching loops</p>

<p>Looks like this focuses only on the quantified theories.</p></li>
</ul>

<ds.algorithms><sat><heuristics>
Understanding performance of QFBV SMT solvers
bennofs
# Understanding performance of QFBV SMT solvers

(Asked by: username_0 on 2017-09-01)

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](http://www.cs.ubc.ca/labs/beta/Projects/SATzilla/SATzilla2012final.pdf): 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](https://bitbucket.org/viperproject/axiom-profiler) A visualization of Z3 instantiation graph and analysis of matching loops

  Looks like this focuses only on the quantified theories.

**Tags:** ds.algorithms, sat, heuristics


---

## 1 answers

### Answer by username_1 on 2017-09-06. Score: 3 | Accepted answer

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.

> **Comments:**
> **username_0**: 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)  

---

