ASKSAGE: Sage Q&A Forum - RSS feedhttps://ask.sagemath.org/questions/Q&A Forum for SageenCopyright Sage, 2010. Some rights reserved under creative commons license.Thu, 25 Oct 2018 16:17:20 +0200Is there anything in Sage which solves #SAT ?https://ask.sagemath.org/question/43984/is-there-anything-in-sage-which-solves-sat/For example using [sharpsat](https://sites.google.com/site/marcthurley/sharpsat) or relsat or Dsharp?Fri, 19 Oct 2018 11:29:29 +0200https://ask.sagemath.org/question/43984/is-there-anything-in-sage-which-solves-sat/Comment by kcrisman for <p>For example using <a href="https://sites.google.com/site/marcthurley/sharpsat">sharpsat</a> or relsat or Dsharp?</p>
https://ask.sagemath.org/question/43984/is-there-anything-in-sage-which-solves-sat/?comment=43993#post-id-43993It's possible you will find [this SAT](http://doc.sagemath.org/html/en/reference/sat/index.html) solver information useful, but probably not since you are a seasoned Sage pro and probably #SAT is not the same thing as SAT ... nonetheless I'll leave this as a comment in case it helps people seeing this know that's not what you're looking for.Fri, 19 Oct 2018 17:35:37 +0200https://ask.sagemath.org/question/43984/is-there-anything-in-sage-which-solves-sat/?comment=43993#post-id-43993Comment by tmonteil for <p>For example using <a href="https://sites.google.com/site/marcthurley/sharpsat">sharpsat</a> or relsat or Dsharp?</p>
https://ask.sagemath.org/question/43984/is-there-anything-in-sage-which-solves-sat/?comment=44001#post-id-44001@kcrisman : SAT is about telling whether there is a solution to some boolean formula, #SAT is about telling how many solutions there are.Sat, 20 Oct 2018 16:41:27 +0200https://ask.sagemath.org/question/43984/is-there-anything-in-sage-which-solves-sat/?comment=44001#post-id-44001Answer by tmonteil for <p>For example using <a href="https://sites.google.com/site/marcthurley/sharpsat">sharpsat</a> or relsat or Dsharp?</p>
https://ask.sagemath.org/question/43984/is-there-anything-in-sage-which-solves-sat/?answer=44000#post-id-44000Since the solutions of a SAT formula corresponds to integer points of some polytope, you can solve #SAT by asking Sage to construct that polytope and count its integer points. See the code below.
The default `integral_points_count` for rational polytopes basically enumerates all integer points, so the choice of the backend could have an importance on the speed. I bet `normaliz` will be faster, it requires the `pynormaliz` optional package to be installed. Please report about your real-life experiments.
Also, the `latte_int` optional package could speed things in some cases, please report your experiments, since that could depend on the actual problem (on the code below, you should use latte=True to use it).
That said for further improvements, we really need to know your real problem.
Typically, the polytopes we consider are included in the unit cube of large dimension, hence I do not see how Barvinok theory (which is what `latte_int` relies on) could speed things up since no set of >=3 points is aligned.
So, depending on your problem, one could imagine to describe it with a "fatter" polytope of smaller dimension, whithout reducing it to SAT first, so that Barvinok theory could be much more efficient.
Other approaches could be thought about too. For example, given a SAT formula, it is easy to enumerate all solution with a SAT solver: for each solution, add its "opposit" as a new constraint and solve it again. I have plans to add such an `__iter__` method to the current SAT solvers in Sage.
def sharp_sat(clauses, backend='cdd', latte=False):
r"""
Count the number of solutions of the given CNF formula.
INPUT:
- clauses is a list of lists of integers representing a CNF formula in the
DIMACS notation, for example:
[[1,2,-3], [-1,2]] means
(x1 or x2 or (not x3)) and ((not 1) or 2)
- backend : one of `'cdd'`, `'normaliz'`, `'ppl'`, `'polymake'`.
- latte : if `True`, use `latte_int` (optional package to be installed) for
the computation.
"""
p = MixedIntegerLinearProgram(solver='ppl')
x = p.new_variable(binary=True)
for clause in clauses:
p.add_constraint(sum([x[i] if i>0 else (1-x[-i]) for i in clause]) >= 1)
P = p.polyhedron(backend=backend)
if latte:
return P.integral_points_count(explicit_enumeration_threshold=0)
else:
return P.integral_points_count()Sat, 20 Oct 2018 16:39:54 +0200https://ask.sagemath.org/question/43984/is-there-anything-in-sage-which-solves-sat/?answer=44000#post-id-44000Comment by Sébastien for <p>Since the solutions of a SAT formula corresponds to integer points of some polytope, you can solve #SAT by asking Sage to construct that polytope and count its integer points. See the code below.</p>
<p>The default <code>integral_points_count</code> for rational polytopes basically enumerates all integer points, so the choice of the backend could have an importance on the speed. I bet <code>normaliz</code> will be faster, it requires the <code>pynormaliz</code> optional package to be installed. Please report about your real-life experiments.</p>
<p>Also, the <code>latte_int</code> optional package could speed things in some cases, please report your experiments, since that could depend on the actual problem (on the code below, you should use latte=True to use it).</p>
<p>That said for further improvements, we really need to know your real problem.</p>
<p>Typically, the polytopes we consider are included in the unit cube of large dimension, hence I do not see how Barvinok theory (which is what <code>latte_int</code> relies on) could speed things up since no set of >=3 points is aligned.</p>
<p>So, depending on your problem, one could imagine to describe it with a "fatter" polytope of smaller dimension, whithout reducing it to SAT first, so that Barvinok theory could be much more efficient.</p>
<p>Other approaches could be thought about too. For example, given a SAT formula, it is easy to enumerate all solution with a SAT solver: for each solution, add its "opposit" as a new constraint and solve it again. I have plans to add such an <code>__iter__</code> method to the current SAT solvers in Sage.</p>
<pre><code>def sharp_sat(clauses, backend='cdd', latte=False):
r"""
Count the number of solutions of the given CNF formula.
INPUT:
- clauses is a list of lists of integers representing a CNF formula in the
DIMACS notation, for example:
[[1,2,-3], [-1,2]] means
(x1 or x2 or (not x3)) and ((not 1) or 2)
- backend : one of `'cdd'`, `'normaliz'`, `'ppl'`, `'polymake'`.
- latte : if `True`, use `latte_int` (optional package to be installed) for
the computation.
"""
p = MixedIntegerLinearProgram(solver='ppl')
x = p.new_variable(binary=True)
for clause in clauses:
p.add_constraint(sum([x[i] if i>0 else (1-x[-i]) for i in clause]) >= 1)
P = p.polyhedron(backend=backend)
if latte:
return P.integral_points_count(explicit_enumeration_threshold=0)
else:
return P.integral_points_count()
</code></pre>
https://ask.sagemath.org/question/43984/is-there-anything-in-sage-which-solves-sat/?comment=44025#post-id-44025Thank you for your idea of using `integral_points_count`. I will compare the speed with dancing links which was the only way I knew to count solutions.Mon, 22 Oct 2018 17:40:06 +0200https://ask.sagemath.org/question/43984/is-there-anything-in-sage-which-solves-sat/?comment=44025#post-id-44025Comment by Sébastien for <p>Since the solutions of a SAT formula corresponds to integer points of some polytope, you can solve #SAT by asking Sage to construct that polytope and count its integer points. See the code below.</p>
<p>The default <code>integral_points_count</code> for rational polytopes basically enumerates all integer points, so the choice of the backend could have an importance on the speed. I bet <code>normaliz</code> will be faster, it requires the <code>pynormaliz</code> optional package to be installed. Please report about your real-life experiments.</p>
<p>Also, the <code>latte_int</code> optional package could speed things in some cases, please report your experiments, since that could depend on the actual problem (on the code below, you should use latte=True to use it).</p>
<p>That said for further improvements, we really need to know your real problem.</p>
<p>Typically, the polytopes we consider are included in the unit cube of large dimension, hence I do not see how Barvinok theory (which is what <code>latte_int</code> relies on) could speed things up since no set of >=3 points is aligned.</p>
<p>So, depending on your problem, one could imagine to describe it with a "fatter" polytope of smaller dimension, whithout reducing it to SAT first, so that Barvinok theory could be much more efficient.</p>
<p>Other approaches could be thought about too. For example, given a SAT formula, it is easy to enumerate all solution with a SAT solver: for each solution, add its "opposit" as a new constraint and solve it again. I have plans to add such an <code>__iter__</code> method to the current SAT solvers in Sage.</p>
<pre><code>def sharp_sat(clauses, backend='cdd', latte=False):
r"""
Count the number of solutions of the given CNF formula.
INPUT:
- clauses is a list of lists of integers representing a CNF formula in the
DIMACS notation, for example:
[[1,2,-3], [-1,2]] means
(x1 or x2 or (not x3)) and ((not 1) or 2)
- backend : one of `'cdd'`, `'normaliz'`, `'ppl'`, `'polymake'`.
- latte : if `True`, use `latte_int` (optional package to be installed) for
the computation.
"""
p = MixedIntegerLinearProgram(solver='ppl')
x = p.new_variable(binary=True)
for clause in clauses:
p.add_constraint(sum([x[i] if i>0 else (1-x[-i]) for i in clause]) >= 1)
P = p.polyhedron(backend=backend)
if latte:
return P.integral_points_count(explicit_enumeration_threshold=0)
else:
return P.integral_points_count()
</code></pre>
https://ask.sagemath.org/question/43984/is-there-anything-in-sage-which-solves-sat/?comment=44070#post-id-44070For an small typical example I have,
sage: p
Boolean Program (maximization, 275 variables, 65 constraints)
sage: p.polyhedron(backend=backend) # takes foreverThu, 25 Oct 2018 16:17:20 +0200https://ask.sagemath.org/question/43984/is-there-anything-in-sage-which-solves-sat/?comment=44070#post-id-44070