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? – Steven Jul 7 at 20:50
• Do you mean DPLL? – Yuval Filmus Jul 7 at 22:32
• The code linked to certainly suggests it. I have no idea what "the recurrency" is, however. – Kyle Jones Jul 7 at 23:56
• @YuvalFilmus en.wikipedia.org/wiki/DPLL_algorithm – Martin Inf1n1ty Jul 8 at 7:36
• Sorry, I have typo mistake – Martin Inf1n1ty Jul 8 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.