<p>I have a problem that could be completely solved as Max-SMT instances in the theory of quantifier-free bit-vectors, but it apparently is too complex to be tractable with current Max-SMT technology.  My application in practice could tolerate a fair amount of error, so I'm interested in the following problem: "Satisfy as many clauses as possible while terminating in <em>x</em> minutes." How would I go about approaching this? Is there a way I can leverage existing solvers?</p>

CC BY-SA 4.0
2018-08-04T01:49:45.250Z
One natural heuristic would be to randomly sample a subset of the constraints, then apply the Max-SMT solver to the resulting subset.
D.W.
CC BY-SA 4.0
2018-08-04T23:47:06.433Z
Some of the MaxSMT and MaxSAT solvers are "anytime" algorithms. They internally compute a sequence of approximations until they find one that cannot be improved (i.e. the optimum). So this should be possible in principle.
Markus
CC BY-SA 4.0
2018-08-04T23:54:03.920Z
The yearly MaxSAT evaluation (https://maxsat-evaluations.github.io/2018/) lists an "incomplete track", which seems to feature exactly this kind of algorithm.
Markus
<approximation-algorithms><sat><max2sat>
Approximate answer to Max-SMT (bitvector) query
lightning
# Approximate answer to Max-SMT (bitvector) query

(Asked by: username_0 on 2018-08-03)

I have a problem that could be completely solved as Max-SMT instances in the theory of quantifier-free bit-vectors, but it apparently is too complex to be tractable with current Max-SMT technology. My application in practice could tolerate a fair amount of error, so I'm interested in the following problem: "Satisfy as many clauses as possible while terminating in *x* minutes." How would I go about approaching this? Is there a way I can leverage existing solvers?

**Tags:** approximation-algorithms, sat, max2sat
> **Comments:**
> **username_1**: One natural heuristic would be to randomly sample a subset of the constraints, then apply the Max-SMT solver to the resulting subset.  
> **username_2**: Some of the MaxSMT and MaxSAT solvers are "anytime" algorithms. They internally compute a sequence of approximations until they find one that cannot be improved (i.e. the optimum). So this should be possible in principle.  
> **username_2**: The yearly MaxSAT evaluation (https://maxsat-evaluations.github.io/2018/) lists an "incomplete track", which seems to feature exactly this kind of algorithm.  

---

## 0 answers

