Add SAT Solver Interface to Reference Manual

[malb]

Sage's SAT solver interface deserves to be in the reference manual.

[ncohen]

HMmmmmm O_o

~/sage/sage$ hgget http://trac.sagemath.org/sage_trac/raw-attachment/ticket/13851/trac_13851.patch
adding trac_13851.patch to series file
applying trac_13851.patch
patching file sage/sat/boolean_polynomials.py
Hunk #2 FAILED at 36
Hunk #4 succeeded at 122 with fuzz 2 (offset 25 lines).
1 out of 6 hunks FAILED -- saving rejects to file sage/sat/boolean_polynomials.py.rej
patch failed, unable to continue (try -v)
patch failed, rejects left in working dir
errors during apply, please fix and refresh trac_13851.patch
~/sage/sage$ 

I use Sage 5.5.rc0. Am I the one at fault there ? :-P

Nathann

[malb]

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 exclusion-clauses using 'solve' from boolean_polynomials.py

so I'll rebase to 5.5.rc0

[malb]

Patch updated.

[ncohen]

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

[malb]

Nathann, I hope this addresses your comments.

[malb]

Updated:

• fixed typo
• running time of cryptominisat.pyx optional doctests is now reasonable.

[ncohen]

Aaaaaaaaaaaaaaaannnnnnnnnnnnnnd it rolls ! Thanks for this patch !!! :-)

Nathann

[jdemeyer]

There is a Sphinx warning:

docstring of sage.misc.classcall_metaclass.ClasscallMetaclass:27: WARNING: more than one target found for cross-reference u'__call__': sage.sat.solvers.dimacs.DIMACS.__call__, sage.sat.converters.polybori.CNFEncoder.__call__

[jhpalmieri]

Removing some dots might make the warning go away:

sage/misc/classcall_metaclass.pyx

@@ -54 +54 @@
      - ``.__classget__`` for customizing the binding behavior in
        ``foo.cls`` (analogue of ``.__get__``).
 
-    See the documentation of :meth:`.__call__` and of :meth:`.__get__`
-    and :meth:`.__contains__` for the description of the respective
+    See the documentation of :meth:`__call__` and of :meth:`__get__`
+    and :meth:`__contains__` for the description of the respective
     protocols.
 
     .. 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?

[jdemeyer]

* ping *

[nthiery]

Replying to jhpalmieri:

Removing some dots might make the warning go away:

sage/misc/classcall_metaclass.pyx

@@ -54 +54 @@
      - ``.__classget__`` for customizing the binding behavior in
        ``foo.cls`` (analogue of ``.__get__``).
 
-    See the documentation of :meth:`.__call__` and of :meth:`.__get__`
-    and :meth:`.__contains__` for the description of the respective
+    See the documentation of :meth:`__call__` and of :meth:`__get__`
+    and :meth:`__contains__` for the description of the respective
     protocols.
 
     .. 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 :-)

[malb]

Thanks everyone! Patch updated.

[ncohen]

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

[ncohen]

O_O

I knew I'd make a mistake with that accent :-P