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 acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

Browse other questions tagged or ask your own question.