3
$\begingroup$

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.

Improve this question
$\endgroup$
1
  • $\begingroup$ 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.) $\endgroup$
    – Brian Borchers
    Commented Jan 28, 2016 at 15:56

1 Answer 1

Reset to default
1
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.