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

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.