#15676: Adding Tseitin's equisatisfiable CNF encodings to symbolic logic module
---------------------------+----------------------------
Reporter: equaeghe | Owner:
Type: enhancement | Status: new
Priority: minor | Milestone: sage-6.1
Component: misc | Keywords:
Merged in: | Authors:
Reviewers: | Report Upstream: N/A
Work issues: | Branch:
Commit: | Dependencies:
Stopgaps: |
---------------------------+----------------------------
Currently, using the symbolic logic module, propositional formulas can be
easily entered. However, as listed in the documentation, the
transformation to CNF is inefficient. Tseitin's equisatisfiable CNF
encodings are efficient (linear increase in size). It may be useful to
include them.
Links:
* module docs:
http://www.sagemath.org/doc/reference/logic/sage/logic/boolformula.html
* Tseitin encoding info: https://en.wikipedia.org/wiki/Tseitin-
Transformation
* Python implementation elsewhere (unfinished?):
https://github.com/cjdrake/pyeda/blob/master/pyeda/boolalg/expr.py#L748
--
Ticket URL: <http://trac.sagemath.org/ticket/15676>
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 unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/sage-trac.
For more options, visit https://groups.google.com/groups/opt_out.
