How Max-SMT solvers do work?

Question

SMT solvers are developed at deal with the satisfiability similar like SAT. As we know, SAT is also for satisfiability and variants of SAT are proposed. One of them is max-SAT. So I want to ask whether there exist max-SMT solvers and if it exists, how does it work?

Answer 1

I'm aware of 3 important strategies. All of them boil down to solving a series of SAT problems. I formulated my answer in terms of hard constraints which must be satisfied and weighted soft constraints which when summed up give you the objective of MAX-SAT.

Linear Search

For a given set of (positively weighted) clauses you have a minimum objective. A minimum objective of 0 would mean that the hard constraint part is satisfiable, a prerequisite for an MAX-SAT solution to even exist.

In a step you try to prove the minimum objective that is strictly bigger than the objective of the previous step. Let's assume we have 3 soft constraints weighted with 2, 3, 7. You would first try to prove (hard constraints + constraint with weight 2), if you are successful you know that the MAX-SAT objective has an lower bound of 2. The smallest lower bound that is strictly better than 2 would be 3. So you would try to prove (hard constraints + constraint with weight 2) if that is also SAT then (hc + 2 + 3) then (hc + 7) then (hc + 7 + 2) then (hc + 7 + 3) then (hc + 7 + 3 + 2).

If you encounter an UNSAT at any point that means that the previous step is the maximum.

Binary Search

If you consider the SAT problems associated with their weight, you might think that solving them is sequentially is a waste since in many cases the previous assignments are not useful. So you could instead try an approach called binary search. The idea is that you pick a problem in the middle of the weight scale, if it is SAT you can discard all problems with weaker weights than it, if it is UNSAT you can discard all problems with higher weights than it. Using this you can find the optimal value in O(log(n)) instead of an expected O(n/2) where n is the number of different weight combinations.

However this approach does not compare as favorable to Linear Search than you might think first. It turns out that UNSAT instaces tend to be way more time intensive than SAT instances. A binary search based MAX-SAT solver tends to have worse anytime behavior that is you don't know when the solver will be stopped and it has to return the best instance it found until then. Any time behavior is important for many real-world applications.

Core driven search

Core driven search is basically a reverse linear search, which runs into a lot of UNSAT instances, however to make up for this it has access to additional information from the solver that might help it skip many intermediate problems.

Core driven search has access to the core of an conflict. So if the solver hits UNSAT it gets a clause that expresses what contradiction existed. It can now take this clause and use it to exclude some weighted soft constraints. By checking which of the are not satisfiable given this clause it can lower the upper bound of the objective and then try again at that bound until it hits a SAT. If it did it knows (since it took the biggest feasible objective) that the current upper bound is the objective.

Summary

For MAX-SAT it is common to solve your problem as series of SAT problems. You can probably also think of some mixed strategies involving these. However there are some different angles to the problem which might be interesting in the future.

Approaches that use the weights to guide one search over all objective values (as you do in Mixed Integer Linear Programming) are not common. This is mostly due to the fact that a braniac MILP approach won't run on industrial instances of the size routinely found in SAT, it is not always obvious how an assignment will affect the soft constraints and that the branching heuristics informed by relaxed solutions are less useful when picking between two values (MAX-SAT can be formulated as 0-1 Integer Linear Program).

There is currently some interesting work by Jakob Nordström around the solver RoundingSAT which uses a formalism called Pseudo Boolean Programming which can encode the same problems as 0-1 ILP and MAX-SAT. PB Optimization has a stronger input format than then CNF used by SAT solvers, is it possible to encode a Pigeon Hole Constraint in two terms instead of an exponential number of terms. However if a PBO solver is given a CNF as input it can't do any of it's more elaborate reasoning and just ends up being a SAT solver that thinks longer per conflict propagation. SAT is dominated by speed demons.

A good longer form presentation going into more technical details is SAT for Optimization by Fahiem Bacchus (University of Toronto).

Answer 2

One of the techniques used to make max-SMT work is the following:

• Augment/formulate the input to allow counting of the number of clauses that evaluate to True in a model(assignment). Call this new formula F, and let the variable K hold the count.

• Perform a binary search on F for optimal (max) possible value of K, by repeatedly calling solver for different fixed values of K.

For example, run the solver on F along with a clause (K = 20).

• If SAT, double the value of K and run solver with (K = 40).

• If UNSAT, halve the value of K and run solver with (K = 10).

Progressively iterate closer to maximal possible value for K.

I know that Yices uses something like this (atleast it used to), however there might be several other optimizations/heuristics added to it.

It is possible that other solvers might use different techniques.

Answer 3

As far as I know, Yices does support max-SMT. Their paper (Archived copy) described a little bit on how it works.