#13120: Improve propositional logic
---------------------------+------------------------------------------------
Reporter: nthiery | Owner: burcin
Type: enhancement | Status: new
Priority: major | Milestone: sage-wishlist
Component: symbolics | Keywords:
Work issues: | Report Upstream: N/A
Reviewers: | Authors:
Merged in: | Dependencies:
Stopgaps: |
---------------------------+------------------------------------------------
I discussed yesterday with Shalom Eliahou and some other persons that
could be interested in using Sage to have a natural syntax for
constructing complicated propositional logic formulas (boolean formulas),
in order to model and treat some of their hard NP problems using SAT
solvers. They currently write directly files in ``sat format'' which is
not necessarily so convenient.
Looking around sage.logic, it feels like this old module could use some
love. Like being more consistent with SymbolicRing in the syntax for
constructing formulas, using Parents/Elements, having interfaces with the
common open source SAT solvers, ... Here are some story suggestions:
{{{
Building formulas::
sage: F = BooleanFormulas();
Boolean formulas
sage: a,b,c = F.var("a,b,c")
sage: ~( (a & b & c) | c )
sage: f = (~(a & b)).equivalent(a|b) # Note: this is backward
incompatible
sage: f.is_tautology()
True
sage: f.parent()
Boolean formulas
sage: f = (a & (a.implies(c))).implies(c)
sage: f.is_tautology()
True
Indexed boolean variables::
sage: x = F.var("x")
sage: (x[1] & x[2]).implies(x[1,3]
(x[1] & x[2]).implies(x[1,3]
Equivalence test::
sage: (~(a & b)).is_equivalent(a|b)
True
Expanding in Conjonctive Normal Form::
sage: f.cnf()
...
Computing an equivalent 3-SAT formula::
sage: f.sat_3()
...
Using SAT solvers::
sage: f.is_satisfiable(solver="mark")
Returning the solutions of f, as an iterable::
sage: S = f.solve(); S
The solutions of ...
sage: for s in S: print s
...
Automatic simplifications
=========================
Associativity::
sage: (a & b) & c
a & b & c
sage: a & (b & c)
a & b & c
sage: a | (b | c)
a | b | c
sage: a | (b | c)
a | b | c
}}}
Of course, a related question is whether one could use one of the
preexisting external libraries for boolean functions.
--
Ticket URL: <http://trac.sagemath.org/sage_trac/ticket/13120>
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 post to this group, send email to [email protected].
To unsubscribe from this group, send email to
[email protected].
For more options, visit this group at
http://groups.google.com/group/sage-trac?hl=en.
