MAXSAT using dpll algorithm?

Question

It's possible to return from a dpll algorithm M as maximum for MAX-SAT problem?:

I have a sample:

https://gist.github.com/davefernig/e670bda722d558817f2ba0e90ebce66f

we can modify recurrency to return the outcome of MAX-SAT?

Resources: https://en.wikipedia.org/wiki/DPLL_algorithm

Answer 1

The DPLL algorithm doesn't try to satisfy as many clauses as possible. If there is a satisfying assignment, DPLL will find it. Otherwise DPLL will try a series of partial assignments until it runs out of possibilities, and then it will declare the formula unsatisfiable. But in the case of an unsatisfiable formula, there is no guarantee that DPLL will discover the maximum number of satisfiable clauses on the way to proving unsatisfiability.

The MAXSAT problem is related to finding the minimally unsatisfiable subformulas (MUSes) of an instance. Determining whether a set of clauses is a MUS is a DP-complete problem. This is expected to be harder than mere NP-completeness, so it is unlikely that modifying DPLL to return partial solutions is going to be fruitful. Given that the class DP is contained in $\Delta^P_2$ you might devise a scheme that calls DPLL (or related algorithms) a polynomial number of times to produce a MAXSAT result.