# optimal SAT solver with weighted variables

I have $n$ boolean variables $x_1,\ldots,x_n$ with associated real-valued costs $c_1,\ldots,c_n$, respectively, and a boolean function $(x_1,\ldots,x_n)\mapsto\Phi(x_1,\ldots,x_n)$ in conjunctive normal form (CNF). I'm looking for a dedicated (ideally free) software package to find an assignment for $x_1,\ldots,x_n$ that satisfies $\Phi$ such that the total cost, that is, the sum of those $c_1,\ldots,c_n$ for which the respective $x_1,\ldots,x_n$ are assigned a true value, is minimised.

My current solution is to convert the problem instance to a binary program and solve that with an implementation of the simplex algorithm + branch and cut (I'm using the GLPK package). I'm wondering whether there are software solutions better tailored for my kind of problem.

• There are certainly faster integer programming codes than GLPK. You should take a look at the academic codes CBC (open source) and SCIP (freely available for academics) and the commercial products CPLEX and Gurobi (also free for academics.) – Brian Borchers Jan 28 '16 at 15:56

## 1 Answer

This is an instance of the Weighted Partial MAX-SAT problem. You could take a look at MAX-SAT solvers; many of them will support this kind of query. For instance, the annual MAX-SAT competition has Weighted Partial MAX-SAT as one of the categories. See here for the results from the 2016 competition. MaxHS looks quite good.

Alternatively, formulate this as an integer linear programming problem and then solve it with any off-the-shelf ILP solver: e.g., CPLEX, Gurobi, CBC, SCIP.