Maximum Satisfiability

<span></span><p dir="ltr"><span><b>The Problem</b></span></p><p dir="ltr"><span>This is a relaxation of boolean satisfiability, though it is still NP-hard. Rather than seeking a solution that satisfies all clauses, it seeks a solution satisfying the maximum number of clauses (</span><a href=""><span></span></a><span>).</span></p><p dir="ltr"><span><b>The Interface</b></span></p><p dir="ltr"><span>The algorithm should take a list of clauses &#160;(in string form, see&#160;</span><a href=""></a>&#160;for an example of how to do the encoding<span>), where we interpret the list of clauses as the conjunction of all of them. &#160;The output should be a HashMap&lt;String,Object&gt; with two keys that contains the solution and number of satisfied clauses. The first key should be &#8220;solution&#8221;, whose value is a HashMap&lt;String,Boolean&gt; in which each key is a variable name and its corresponding value is it&#8217;s truth assignment in the solution. The second key is a string &#8220;maxSatisfied&#8221;, whose value is the number of clauses satisfied (an int).</span></p><p dir="ltr"><span><b>The Algorithm</b></span></p><span>The simplest solution would probably be to build this on top of Binary Integer Programming (</span><a href=""><span></span></a><span>), which is itself built on top of JaCoP (</span>
Fulfilled By
  • Max-Sat


    This algorithm solves the unweighted partial maximum satisfiability problem by invoking a fast SAT solver repeatedly.

    • requests
  • /

    • requests


  • {{comment.username}}
Bounty expires in
Bounty expired
(no tags)