1
$\begingroup$

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?

$\endgroup$
3
  • 1
    $\begingroup$ It depends on which constraints you allow. What domain do the variables fall into? Are they booleans? Integers? Real numbers? Something else? What kinds of constraints do you allow? I hope you can edit the question to clarify those points. $\endgroup$
    – D.W. ♦
    Jun 7, 2020 at 2:01
  • $\begingroup$ Yes, I can update to answer these questions. I thought since the problem is #SAT, I assumed the domain of variables was clear. $\endgroup$
    – Rikard Olsson
    Jun 7, 2020 at 19:15
  • $\begingroup$ Yes, please edit to state that, as it wasn't clear to me. Thank you! $\endgroup$
    – D.W. ♦
    Jun 7, 2020 at 23:20

3 Answers 3

Reset to default
2
+50
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Thanks for this comprehensive answer. I did look into the first approach which seam to suit well. What I did not talk about in the question was that there seam to be a much simpler way to describe xor's in mathematical constraints than CNF, which was one of the reasons why I was looking for a way to count using constraints. $\endgroup$
    – Rikard Olsson
    Jun 13, 2020 at 11:17
0
$\begingroup$

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).

$\endgroup$
1
  • $\begingroup$ 1. SAT solvers typically use DPLL-based methods, but I have the impression that many #SAT solvers use other methods. I'm not sure whether that is accurate. 2. DPLL-based solvers typically rely on conflict-driven clause learning, non-chronological backtracking, and heuristics for efficiency. It seems like it would take some nontrivial work to figure out how to generalize those to constraints instead of CNF clauses, and I'm not sure whether all of them would have natural generalizations. Without them, it seems like there might be a significant loss of efficiency. $\endgroup$
    – D.W. ♦
    Jun 10, 2020 at 20:32
0
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ If my understandings are correct, this will return not only how many feasible solutions but also the actual points. Not only that, I’ll have to set a parameter M telling the maximum number of solutions to return: ”... choose a really large value of M and hope you live long enough to see the run terminate.”. But maybe I missunderstood the solution. $\endgroup$
    – Rikard Olsson
    Jun 9, 2020 at 18:53
  • $\begingroup$ You must be referring to a specific implementation or post here, and I don't know which one. But yes any such algorithm can return the actual points as well. $\endgroup$
    – Ggouvine
    Jun 9, 2020 at 19:40
  • $\begingroup$ This approach enumerates all of the solutions. Thus I expect it will be slow if there are many solutions. There are other methods that are faster than enumerating all the solutions -- counting the number of solutions can be faster than enumerating the solutions. $\endgroup$
    – D.W. ♦
    Jun 10, 2020 at 20:29
  • $\begingroup$ Definitely. A simple one for #SAT is to stop when a satisfiable solution is reached, and count $2^k$ solutions if there are $k$ unassigned litterals. $\endgroup$
    – Ggouvine
    Jun 10, 2020 at 20:37
  • $\begingroup$ However, the question is asking about mathematical models. I'd argue that the SAT approach that you're advocating is not suited for them and will generally be much slower. LP relaxation and cuts are critical components of an efficient math solver. $\endgroup$
    – Ggouvine
    Jun 10, 2020 at 20:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.