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?