Sage: Ticket #13120: Improve propositional logic
https://trac.sagemath.org/ticket/13120
<p>
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 <code></code>sat format<em> which is not necessarily so convenient.
</em></p>
<p>
Looking around sage.logic, it feels like this old module could use some love. Like being more consistent with <a class="missing wiki">SymbolicRing?</a> in the syntax for constructing formulas, using <a class="missing wiki">Parents/Elements?</a>, having interfaces with the common open source SAT solvers, ... Here are some story suggestions:
</p>
<pre class="wiki">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
</pre><p>
Of course, a related question is whether one could use one of the preexisting external libraries for boolean functions.
</p>
en-usSagehttps://trac.sagemath.org/chrome/site/logo_sagemath_trac.png
https://trac.sagemath.org/ticket/13120
Trac 1.1.6kiniFri, 15 Jun 2012 22:19:32 GMTcc changed
https://trac.sagemath.org/ticket/13120#comment:1
https://trac.sagemath.org/ticket/13120#comment:1
<ul>
<li><strong>cc</strong>
<em>kini</em> added
</li>
</ul>
TicketjlopezFri, 15 Jun 2012 22:28:43 GMT
https://trac.sagemath.org/ticket/13120#comment:2
https://trac.sagemath.org/ticket/13120#comment:2
<p>
You might want to make this building upon <a class="closed ticket" href="https://trac.sagemath.org/ticket/418" title="enhancement: Add SAT Solvers (closed: fixed)">#418</a> (needing review)
</p>
Ticket