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?

  • $\begingroup$ One natural heuristic would be to randomly sample a subset of the constraints, then apply the Max-SMT solver to the resulting subset. $\endgroup$ – D.W. Aug 4 '18 at 1:49
  • $\begingroup$ 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. $\endgroup$ – Markus Aug 4 '18 at 23:47
  • $\begingroup$ The yearly MaxSAT evaluation (maxsat-evaluations.github.io/2018) lists an "incomplete track", which seems to feature exactly this kind of algorithm. $\endgroup$ – Markus Aug 4 '18 at 23:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.