#19042: Fallback SAT solver in Sage
-------------------------+-------------------------------------------------
Reporter: | Owner:
ncohen | Status: needs_review
Type: | Milestone: sage-6.9
enhancement | Resolution:
Priority: major | Merged in:
Component: | Reviewers:
numerical | Work issues:
Keywords: | Commit:
Authors: | eb01119cd733a39fd72aabfc7feb2114115d1526
Nathann Cohen | Stopgaps:
Report Upstream: N/A |
Branch: |
public/19042 |
Dependencies: |
-------------------------+-------------------------------------------------
Comment (by jdemeyer):
Replying to [comment:10 ncohen]:
> But the doc of the same function in cryptominisat says that the function
returns None when it is interrupted.
I don't believe that doc. From an example based on a doctest:
{{{
sage: from sage.sat.solvers import CryptoMiniSat # optional -
cryptominisat
sage: from sage.sat.converters.polybori import CNFEncoder # optional -
cryptominisat
sage: set_random_seed( 22 ) # optional -
cryptominisat
sage: sr = mq.SR(1,4,4,4,gf2=True,polybori=True) # optional -
cryptominisat
sage: F,s = sr.polynomial_system() # optional -
cryptominisat
sage: cms = CryptoMiniSat(maxrestarts=10,verbosity=0) # optional -
cryptominisat
sage: phi = CNFEncoder(cms, F.ring())(F) # optional -
cryptominisat
sage: alarm(0.2); cms()
---------------------------------------------------------------------------
AlarmInterrupt Traceback (most recent call
last)
<ipython-input-8-257eb3253d78> in <module>()
----> 1 alarm(RealNumber('0.2')); cms()
/usr/local/src/sage-
config/src/sage/sat/solvers/cryptominisat/cryptominisat.pyx in
sage.sat.solvers.cryptominisat.cryptominisat.CryptoMiniSat.__call__
(build/cythonized/sage/sat/solvers/cryptominisat/cryptominisat.cpp:2211)()
299 cdef lbool r
300 if assumptions is None:
--> 301 sig_on()
302 r = self._solver.solve()
303 sig_off()
/usr/local/src/sage-config/src/sage/ext/interrupt/interrupt.pyx in
sage.ext.interrupt.interrupt.sig_raise_exception
(build/cythonized/sage/ext/interrupt/interrupt.c:957)()
88 raise KeyboardInterrupt
89 if sig == SIGALRM:
---> 90 raise AlarmInterrupt
91 if sig == SIGILL:
92 if msg == NULL:
AlarmInterrupt:
}}}
--
Ticket URL: <http://trac.sagemath.org/ticket/19042#comment:11>
Sage <http://www.sagemath.org>
Sage: Creating a Viable Open Source Alternative to Magma, Maple, Mathematica,
and MATLAB
--
You received this message because you are subscribed to the Google Groups
"sage-trac" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/sage-trac.
For more options, visit https://groups.google.com/d/optout.
