# MAXSAT using dpll algorithm?

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?

• Maybe you can add a description of the "dppl algorithm" to your question? Jul 7 '20 at 20:50
• Do you mean DPLL? Jul 7 '20 at 22:32
• The code linked to certainly suggests it. I have no idea what "the recurrency" is, however. Jul 7 '20 at 23:56
• @YuvalFilmus en.wikipedia.org/wiki/DPLL_algorithm Jul 8 '20 at 7:36
• Sorry, I have typo mistake Jul 8 '20 at 7:36

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.