Opened 7 years ago

Closed 7 years ago

Last modified 7 years ago

#13851 closed enhancement (fixed)

Add SAT Solver Interface to Reference Manual

Reported by: malb Owned by: mvngu
Priority: major Milestone: sage-5.6
Component: documentation Keywords:
Cc: ncohen, nthiery, hivert Merged in: sage-5.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)

trac_13851.patch (19.4 KB) - added by malb 7 years ago.

Download all attachments as: .zip

Change History (19)

comment:1 Changed 7 years ago by ncohen

  • Status changed from new to needs_review

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

comment:2 Changed 7 years ago by 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

comment:3 Changed 7 years ago by malb

Patch updated.

comment:4 Changed 7 years ago by ncohen

  • 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 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

comment:5 Changed 7 years ago by malb

Nathann, I hope this addresses your comments.

comment:6 Changed 7 years ago by malb

Updated:

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

comment:7 Changed 7 years ago by ncohen

  • Status changed from needs_work to positive_review

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

Nathann

comment:8 Changed 7 years ago by jdemeyer

  • Authors set to Martin Albrecht
  • Reviewers set to Nathann Cohen

comment:9 Changed 7 years ago by jdemeyer

  • 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 cross-reference u'__call__': sage.sat.solvers.dimacs.DIMACS.__call__, sage.sat.converters.polybori.CNFEncoder.__call__

comment:10 follow-up: Changed 7 years ago by jhpalmieri

  • 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 
    5454     - ``.__classget__`` for customizing the binding behavior in
    5555       ``foo.cls`` (analogue of ``.__get__``).
    5656
    57     See the documentation of :meth:`.__call__` and of :meth:`.__get__`
    58     and :meth:`.__contains__` for the description of the respective
     57    See the documentation of :meth:`__call__` and of :meth:`__get__`
     58    and :meth:`__contains__` for the description of the respective
    5959    protocols.
    6060
    6161    .. 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 jdemeyer

* ping *

comment:12 in reply to: ↑ 10 Changed 7 years ago by nthiery

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 
    5454     - ``.__classget__`` for customizing the binding behavior in
    5555       ``foo.cls`` (analogue of ``.__get__``).
    5656
    57     See the documentation of :meth:`.__call__` and of :meth:`.__get__`
    58     and :meth:`.__contains__` for the description of the respective
     57    See the documentation of :meth:`__call__` and of :meth:`__get__`
     58    and :meth:`__contains__` for the description of the respective
    5959    protocols.
    6060
    6161    .. 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 malb

comment:13 Changed 7 years ago by malb

  • Status changed from needs_work to needs_review

Thanks everyone! Patch updated.

comment:14 Changed 7 years ago by ncohen

  • 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 ncohen

  • Reviewers changed from Nathann Cohen to Nathann Cohen, John H. Palmieri, Nicolas M. Thièry

comment:16 Changed 7 years ago by ncohen

  • 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 jdemeyer

  • Merged in set to sage-5.6.rc0
  • Resolution set to fixed
  • Status changed from positive_review to closed

comment:18 Changed 7 years ago by jdemeyer

  • Reviewers changed from Nathann Cohen, John H. Palmieri, Nicolas M. Thiéry to Nathann Cohen, John Palmieri, Nicolas M. Thiéry
Note: See TracTickets for help on using tickets.