# 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.) Jan 28 '16 at 15:56