Counting the number of satisfied models - given mathematical constraints

Question

Question

There are plenty of algorithms for solving the #SAT problem, with one being the DPLL algorithm and is implemented for all kinds of programming languages. As far as I've seen, they all take a boolean formula on CNF as input and outputs the number of satisfied interpretations.

Mathematical constraints, on the other hand, is another way defining an instance of SAT-problem and is often used in discrete optimization, where one tries to optimize some function with respect to these constraints. Is there a program taking mathematical constraints as input and outputs the number of satisfied interpretations?

Example

We represent the boolean formula $Q = (a \lor b) \wedge (c \lor d)$ as constraints as $$a + b \geq 1 \\ c + d \geq 1$$ or as a matrix $A$ and support vector $b$ $$ A= \begin{bmatrix} 1 & 1 & 0 & 0 \\ 0 & 0 & 1 & 1 \end{bmatrix} \\ b = \begin{bmatrix} 1 & 1 \end{bmatrix} $$

where all variables $a,b,c,d \in \{0,1\}$. We know there are programs taking $Q$ as input and outputs the number of interpretations but are there programs taking $A$ and $b$ as input (or similar construction) and outputs the same number of interpretations?

Answer 1

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 doing that, which you could apply directly. If you search on "counting integer points in polytope" or "counting lattice points in polytope" you'll find many research papers. See, e.g., https://cstheory.stackexchange.com/q/22280/5038, Finding all solutions to an integer linear programming (ILP) problem.

Approach #2: Convert to CNF, then use a #SAT solver.

You can always convert your constraints to a CNF formula. Each linear inequality can be converted to a set of CNF clauses. A linear inequality of the form $x_i + \dots + x_j \ge 1$ corresponds immediately to the CNF clause $(x_i \lor \dots \lor x_j)$. For a more general linear inequality of the form $x_i + \dots + x_j \ge c$, you want to express the constraint that at least $c$ out of the $k$ variables $x_i,\dots,x_j$ are true. There are many standard ways of encoding that. See https://cstheory.stackexchange.com/q/23771/5038, Reduce the following problem to SAT, Encoding 1-out-of-n constraint for SAT solvers,

(One approach is to convert a Boolean circuit that computes $x_i + \dots + x_j$ and compares it to $c$, then convert the Boolean circuit to CNF using the Tseitin transform. You can create such a Boolean circuit by using standard adder and comparator circuits. However, there are many other ways as well.)

Once you have a CNF formula that is equivalent to the set of constraints, then you can use any off-the-shelf #SAT solver to count the number of solutions to that CNF formula.

---

It's hard to say which of these two approaches will work better; you might need to try them both on the kinds of instances you're dealing with, to know for sure. I'd expect that if you have linear inequalities of the form $x_i + \dots + x_j \ge c$ where $c$ is large, then Approach #1 may be superior; but if $c$ is typically small, then Approach #2 may be superior.

Answer 2

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.

The rest of the algorithm remains the same.

A constraint over boolean variables is just a collection of hidden CNF clauses (potentially exponentially many clauses depending on the constraint).

Answer 3

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.