New answers tagged


I know of two reasonable approaches. Approach #1: Count the number of integer points inside a convex polytope. The set of linear inequalities you provided, together with the inequalities $0 \le a,b,c,d \le 1$, defines a convex polytope. Now, you want to count the number of integer points that fall within this polytope. There are standard algorithms for ...


The question has been answered on or.stackexchange for Mixed-Integer Programming software, with examples of existing software and scripts (CPLEX, SCIP, ...). This is more similar to the CDCL algorithm than to DPLL: when a new solution is found, a new constraint is added to forbid it and the search resumes, until the problem becomes infeasible.


You can implement DPLL using directly using the constraints instead of clauses. This requires modifying the data structure and the propagation algorithm, but it works all the same. As soon as all the variables of the constraint are set except one, unit propagation may occur. As soon as all the variables of the constraint are set, a conflict may occur. ...

Top 50 recent answers are included