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.Fri, 19 Oct 2018 11:29:29 +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?SébastienFri, 19 Oct 2018 11:29:29 +0200https://ask.sagemath.org/question/43984/Non linear Binary equations using sat solverhttps://ask.sagemath.org/question/36165/non-linear-binary-equations-using-sat-solver/ How can I solve a set of nonlinear binary equations in SAGE using the sat solver?RADEON360Wed, 04 Jan 2017 07:25:06 +0100https://ask.sagemath.org/question/36165/CryptoMiniSat assertion errorhttps://ask.sagemath.org/question/27039/cryptominisat-assertion-error/I'm trying to use `sage.sat.boolean_polynomials` to solve a system of equations for my thesis. I'm ok with the fact it uses CryptoMiniSat as default but every time I run my script I get this error:
Traceback (most recent call last):
File "simon_equations.py", line 104, in <module>
s = alg_attack(p,c)
File "simon_equations.py", line 55, in alg_attack
return solve_sat(F)
File "/home/frollo/sage-6.7/local/lib/python2.7/site-packages/sage/sat/boolean_polynomials.py", line 179, in solve
phi = converter(F)
File "/home/frollo/sage-6.7/local/lib/python2.7/site-packages/sage/sat/converters/polybori.py", line 581, in __call__
self.clauses(f)
File "/home/frollo/sage-6.7/local/lib/python2.7/site-packages/sage/sat/converters/polybori.py", line 538, in clauses
self.clauses_sparse(f)
File "/home/frollo/sage-6.7/local/lib/python2.7/site-packages/sage/sat/converters/polybori.py", line 296, in clauses_sparse
self.solver.add_clause(clause(c))
File "sage/sat/solvers/cryptominisat/cryptominisat.pyx", line 205, in sage.sat.solvers.cryptominisat.cryptominisat.CryptoMiniSat.add_clause (build/cythonized/sage/sat/solvers/cryptominisat/cryptominisat.cpp:1672)
AssertionError
I got to line 205 of sage/sat/solvers/cryptominisat/cryptominisat.pyx and found this:
assert(self._solver.okay())
I found nothing about this in the documentation, so I decided to try some bad practices and commented away the assertion, restarted sage and tried again. I got the same error, referring to a line that is now a comment. I tried to restart my shell but, again, I got the same error.
Has anyone a clue about which could be causing this (the same script worked during the tests, the error just started showing up when I tried to run something serious)frolloSat, 06 Jun 2015 18:21:20 +0200https://ask.sagemath.org/question/27039/SAT Solverhttps://ask.sagemath.org/question/10664/sat-solver/From the documentation of `sage.sat.boolean_polynomials.solve` ([here](http://www.sagemath.org/doc/reference/sat/sage/sat/boolean_polynomials.html)), it is not clear how to use it. Can anyone cite me any detailed example?
Say, I need to solve (in a Boolean ring)
<code> (x1 + x2 * x3 = x2)*(x2 = x3) </code>.
Can we do it?
Regards.ppSun, 03 Nov 2013 22:44:00 +0100https://ask.sagemath.org/question/10664/SAT Solver outputhttps://ask.sagemath.org/question/10680/sat-solver-output/I need to solve a SAT problem. I searched and found the manual [here](http://www.sagemath.org/doc/reference/sat/), but can not figure out the output obtained:
sage: from sage.sat.solvers import CryptoMiniSat # optional - cryptominisat
sage: cms = CryptoMiniSat() # optional - cryptominisat
sage: cms.add_clause((1,2,-3)) # optional - cryptominisat
sage: cms() # optional - cryptominisat
(None, True, True, False)
There are 3 variables, then what does that `None` mean?ppFri, 01 Nov 2013 02:21:06 +0100https://ask.sagemath.org/question/10680/SAT Math Level 2 Subject Test Sample Question #26https://ask.sagemath.org/question/7737/sat-math-level-2-subject-test-sample-question-26/A circle has a radius of 2. Two different tangent lines intersect the circle at points D and E. Those same tangent lines intersect each other outside the circle at point F, forming an acute angle of 50 degrees. If a chord is drawn between D and E, what is its length?ccanoncWed, 20 Oct 2010 12:18:26 +0200https://ask.sagemath.org/question/7737/SAT Math Level 2 Subject Test Sample Question #19https://ask.sagemath.org/question/7733/sat-math-level-2-subject-test-sample-question-19/What is the limit of $f(x)$ as $x$ approaches infinity, for $f(x) = (4*3 + 3x) / (-12 + 2x)$ ?ccanoncMon, 18 Oct 2010 15:28:00 +0200https://ask.sagemath.org/question/7733/