# #StackBounty: #satisfiability #constraint-satisfaction Counting the number of satisfied models – given mathematical constraints

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

Get this bounty!!!

This site uses Akismet to reduce spam. Learn how your comment data is processed.