Maximum Satisfiability

Description
<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="http://en.wikipedia.org/wiki/Maximum_satisfiability_problem"><span>http://en.wikipedia.org/wiki/Maximum_satisfiability_problem</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="http://algorithmia.com/algorithms/cloncaric/sat">http://algorithmia.com/algorithms/cloncaric/sat</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="https://algorithmia.com/algorithms/JaCoP/BinaryIntegerProgramming"><span>https://algorithmia.com/algorithms/JaCoP/BinaryIntegerProgramming</span></a><span>), which is itself built on top of JaCoP (http://www.jacop.eu/).</span>
Fulfilled By
  • This algorithm solves the unweighted partial maximum satisfiability problem by invoking a fast SAT solver repeatedly.
    • requests
Discussion
  • {{comment.username}}
Status
Fulfilled
Bounty expires in
Bounty expired
Bounty
20
Tags
(no tags)