#13851 closed enhancement (fixed)
Add SAT Solver Interface to Reference Manual
Reported by:  malb  Owned by:  mvngu 

Priority:  major  Milestone:  sage5.6 
Component:  documentation  Keywords:  
Cc:  ncohen, nthiery, hivert  Merged in:  sage5.6.rc0 
Authors:  Martin Albrecht  Reviewers:  Nathann Cohen, John Palmieri, Nicolas M. Thiéry 
Report Upstream:  N/A  Work issues:  
Branch:  Commit:  
Dependencies:  Stopgaps: 
Description
Sage's SAT solver interface deserves to be in the reference manual.
Attachments (1)
Change History (19)
comment:1 Changed 7 years ago by
 Status changed from new to needs_review
comment:2 Changed 7 years ago by
Indeed, 5.5.rc0 has
changeset: 17452:464c7dc09aa9 user: Philipp Jovanovic <p.jo@gmx.net> date: Mon Oct 08 15:45:37 2012 +0200 summary: Trac #13575: Add flexibility when creating exclusionclauses using 'solve' from boolean_polynomials.py
so I'll rebase to 5.5.rc0
comment:3 Changed 7 years ago by
Patch updated.
comment:4 Changed 7 years ago by
 Status changed from needs_review to needs_work
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 toNone
, 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/sage2/doc/en/reference$ sage t long optional sat.rst sage t long optional "devel/sage2/doc/en/reference/sat.rst" ********************************************************************** File "/home/ncohen/.Sage/devel/sage2/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
comment:5 Changed 7 years ago by
Nathann, I hope this addresses your comments.
comment:6 Changed 7 years ago by
Updated:
 fixed typo
 running time of cryptominisat.pyx optional doctests is now reasonable.
comment:7 Changed 7 years ago by
 Status changed from needs_work to positive_review
Aaaaaaaaaaaaaaaannnnnnnnnnnnnnd it rolls ! Thanks for this patch !!! :)
Nathann
comment:8 Changed 7 years ago by
 Reviewers set to Nathann Cohen
comment:9 Changed 7 years ago by
 Status changed from positive_review to needs_work
There is a Sphinx warning:
docstring of sage.misc.classcall_metaclass.ClasscallMetaclass:27: WARNING: more than one target found for crossreference u'__call__': sage.sat.solvers.dimacs.DIMACS.__call__, sage.sat.converters.polybori.CNFEncoder.__call__
comment:10 followup: ↓ 12 Changed 7 years ago by
 Cc nthiery hivert added
Removing some dots might make the warning go away:

sage/misc/classcall_metaclass.pyx
diff git a/sage/misc/classcall_metaclass.pyx b/sage/misc/classcall_metaclass.pyx
a b cdef class ClasscallMetaclass(NestedClas 54 54  ``.__classget__`` for customizing the binding behavior in 55 55 ``foo.cls`` (analogue of ``.__get__``). 56 56 57 See the documentation of :meth:` .__call__` and of :meth:`.__get__`58 and :meth:` .__contains__` for the description of the respective57 See the documentation of :meth:`__call__` and of :meth:`__get__` 58 and :meth:`__contains__` for the description of the respective 59 59 protocols. 60 60 61 61 .. warning:: for technical reasons, ``__classcall__``,
But I'm not sure if this change has other effects. I couldn't see any, but I really don't know. The dots seem to have been added in #8250. Florent or Nicolas, is it okay if we get rid of them?
comment:11 Changed 7 years ago by
* ping *
comment:12 in reply to: ↑ 10 Changed 7 years ago by
Replying to jhpalmieri:
Removing some dots might make the warning go away:
sage/misc/classcall_metaclass.pyx
diff git a/sage/misc/classcall_metaclass.pyx b/sage/misc/classcall_metaclass.pyx
a b cdef class ClasscallMetaclass(NestedClas 54 54  ``.__classget__`` for customizing the binding behavior in 55 55 ``foo.cls`` (analogue of ``.__get__``). 56 56 57 See the documentation of :meth:` .__call__` and of :meth:`.__get__`58 and :meth:` .__contains__` for the description of the respective57 See the documentation of :meth:`__call__` and of :meth:`__get__` 58 and :meth:`__contains__` for the description of the respective 59 59 protocols. 60 60 61 61 .. warning:: for technical reasons, ``__classcall__``, But I'm not sure if this change has other effects. I couldn't see any, but I really don't know. The dots seem to have been added in #8250. Florent or Nicolas, is it okay if we get rid of them?
Gosh, I had already answered that! I guess the trac connection expired without me noticing. Oh well.
The change is fine for me. I usually don't put them anyway :)
Changed 7 years ago by
comment:13 Changed 7 years ago by
 Status changed from needs_work to needs_review
Thanks everyone! Patch updated.
comment:14 Changed 7 years ago by
 Status changed from needs_review to positive_review
Well, it passed all long tests on my machine, and there was no problem with the doc after I removed output/ and built it again. Should be good now :P
Thaaaaaaaaaaaaaaanks !!!
Nathann
comment:15 Changed 7 years ago by
 Reviewers changed from Nathann Cohen to Nathann Cohen, John H. Palmieri, Nicolas M. Thièry
comment:16 Changed 7 years ago by
 Reviewers changed from Nathann Cohen, John H. Palmieri, Nicolas M. Thièry to Nathann Cohen, John H. Palmieri, Nicolas M. Thiéry
O_O
I knew I'd make a mistake with that accent :P
comment:17 Changed 7 years ago by
 Merged in set to sage5.6.rc0
 Resolution set to fixed
 Status changed from positive_review to closed
comment:18 Changed 7 years ago by
 Reviewers changed from Nathann Cohen, John H. Palmieri, Nicolas M. Thiéry to Nathann Cohen, John Palmieri, Nicolas M. Thiéry
HMmmmmm
O_o
I use Sage 5.5.rc0. Am I the one at fault there ?
:P
Nathann