*Bounty: 50*

*Bounty: 50*

## 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?