#13851: Add SAT Solver Interface to Reference Manual
---------------------------------+------------------------------------------
Reporter: malb | Owner: mvngu
Type: enhancement | Status: needs_work
Priority: major | Milestone: sage-5.6
Component: documentation | Resolution:
Keywords: | Work issues:
Report Upstream: N/A | Reviewers:
Authors: | Merged in:
Dependencies: | Stopgaps:
---------------------------------+------------------------------------------
Changes (by ncohen):
* status: needs_review => needs_work
Comment:
Hellooooooooooooo Martin !!!
Well, I think that this is a nice thing indeed to add to Sage ! It will
certainly help make the use of sage.sat clearer `:-)`
Some comments :
* looking at the sat.rst file, I think that it would be better to put the
"table of contents" above the introduction. It is easy to see on one
screen that the files includes the introduction, but it is hard to guess
that there is a table of contents afterwards. To me it seems better the
other way around, but that's up to you.
* I am also use to see some title before the automatically generated list
of classes and methods. It helps differentiate visually what is the
"introduction" and what is the list of functions. Again, that's up to you.
* It may be totally obvious when you deal with SAT solvers, but I wondered
what the input format of `add_clause` was. Looks like -2 represents the
negation of variable 2, it's the kind of thing that could be written
somewhere, just to make sure in case of doubt.
* You say in `add_clause` that new variables are created if necessary when
a new number appears. Does it mean that 1000000 variables will be created
if I add a clause containing variable 1000000, or just one new variable
corresponding to 1000000 ? It would be nice to add this information
somewhere, too.
* What happens when `.write` is called and the filename it set to `None`,
its default value ? I guess an exception should be raised in that case,
but it depends on the answer `:-)`
I read the doc of "Anf to CNF" and the doc of "Sat functions for
polynomials", and even though it took me some time to understand what it
was about, it felt like "beginner's questions", and unclear only because
it is not my field. If you feel that this doc is sufficient then let it go
into Sage, having this exposed is nice enough for a start and I cannot
tell what could miss either `:-)`
About tests:
* sat.rst does not pass optional doctests
{{{
~/.Sage/devel/sage-2/doc/en/reference$ sage -t -long -optional sat.rst
sage -t -long -optional "devel/sage-2/doc/en/reference/sat.rst"
**********************************************************************
File "/home/ncohen/.Sage/devel/sage-2/doc/en/reference/sat.rst", line 77:
sage: s = solve_sat(F) #
optional - cryptominisat
Exception raised:
Traceback (most recent call last):
File "/home/ncohen/.Sage/local/bin/ncadoctest.py", line 1231, in
run_one_test
self.run_one_example(test, example, filename, compileflags)
File "/home/ncohen/.Sage/local/bin/sagedoctest.py", line 38, in
run_one_example
OrigDocTestRunner.run_one_example(self, test, example, filename,
compileflags)
File "/home/ncohen/.Sage/local/bin/ncadoctest.py", line 1172, in
run_one_example
compileflags, 1) in test.globs
File "<doctest __main__.example_6[3]>", line 1, in <module>
s = solve_sat(F) #
optional - cryptominisat###line 77:
sage: s = solve_sat(F) #
optional - cryptominisat
NameError: name 'F' is not defined
**********************************************************************
}}}
* cryptominisat.pyx does not pass doctests either, and it is... Pretty
long `:-P`
Nathann
Nathann
--
Ticket URL: <http://trac.sagemath.org/sage_trac/ticket/13851#comment:4>
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 post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/sage-trac?hl=en.
