#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)
Change History (19)
comment:1 Changed 8 years ago by
- Status changed from new to needs_review
comment:2 Changed 8 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 exclusion-clauses using 'solve' from boolean_polynomials.py
so I'll rebase to 5.5.rc0
comment:3 Changed 8 years ago by
Patch updated.
comment:4 Changed 8 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/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 8 years ago by
Nathann, I hope this addresses your comments.
comment:6 Changed 8 years ago by
Updated:
- fixed typo
- running time of cryptominisat.pyx optional doctests is now reasonable.
comment:7 Changed 8 years ago by
- Status changed from needs_work to positive_review
Aaaaaaaaaaaaaaaannnnnnnnnnnnnnd it rolls ! Thanks for this patch !!! :-)
Nathann
comment:8 Changed 8 years ago by
- Reviewers set to Nathann Cohen
comment:9 Changed 8 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 cross-reference u'__call__': sage.sat.solvers.dimacs.DIMACS.__call__, sage.sat.converters.polybori.CNFEncoder.__call__
comment:10 follow-up: ↓ 12 Changed 8 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 8 years ago by
* ping *
comment:12 in reply to: ↑ 10 Changed 8 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 8 years ago by
comment:13 Changed 8 years ago by
- Status changed from needs_work to needs_review
Thanks everyone! Patch updated.
comment:14 Changed 8 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 8 years ago by
- Reviewers changed from Nathann Cohen to Nathann Cohen, John H. Palmieri, Nicolas M. Thièry
comment:16 Changed 8 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 8 years ago by
- Merged in set to sage-5.6.rc0
- Resolution set to fixed
- Status changed from positive_review to closed
comment:18 Changed 8 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