<span></span><p dir="ltr"><span><b>The Problem</b></span></p><p dir="ltr"><span>This is a generalization of the maximum satisfiability problem (a seperate bounty) is briefly described in </span><a href="http://en.wikipedia.org/wiki/Maximum_satisfiability_problem"><span>http://en.wikipedia.org/wiki/Maximum_satisfiability_problem</span></a><span>. Each clause has a corresponding weight, and the weight of a solution is just the sum of the weights of the clauses that are satisfied in that solution. The goal is to maximize this weight. Note that maximum satisfiability is just this problem with every clause weight equal to 1.</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, as well as a list of doubles, where the ith double in the list is the weight of the ith clause.  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 “weight”, whose value is the number of the total weight of  satisfied clauses (a double).</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 (</span><a href="http://www.jacop.eu/"><span>http://www.jacop.eu/</span></a><span>).</span>