Opened 9 years ago

Last modified 9 years ago

#13120 new enhancement

Improve propositional logic

Reported by: nthiery Owned by: burcin
Priority: major Milestone: sage-wishlist
Component: symbolics Keywords:
Cc: eliahou@…, kini Merged in:
Authors: Reviewers:
Report Upstream: N/A Work issues:
Branch: Commit:
Dependencies: Stopgaps:

Status badges

Description

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.

Change History (2)

comment:1 Changed 9 years ago by kini

  • Cc kini added

comment:2 Changed 9 years ago by jlopez

You might want to make this building upon #418 (needing review)

Last edited 9 years ago by jlopez (previous) (diff)
Note: See TracTickets for help on using tickets.