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

I have a sample:


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

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

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

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.