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  (in string form, see </span><a href="http://algorithmia.com/algorithms/cloncaric/sat">http://algorithmia.com/algorithms/cloncaric/sat</a> for an example of how to do the encoding<span>), where we interpret the list of clauses as the conjunction of all of them.  The output should be a HashMap<String,Object> with two keys that contains the solution and number of satisfied clauses. The first key should be “solution”, whose value is a HashMap<String,Boolean> in which each key is a variable name and its corresponding value is it’s truth assignment in the solution. The second key is a string “maxSatisfied”, 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>
