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

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?


Get this bounty!!!

Leave a Reply

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