Opened 8 years ago

Last modified 7 years ago

#15676 new enhancement

Adding Tseitin's equisatisfiable CNF encodings to symbolic logic module

Reported by: equaeghe Owned by:
Priority: minor Milestone: sage-6.4
Component: misc Keywords:
Cc: Merged in:
Authors: Reviewers:
Report Upstream: N/A Work issues:
Branch: Commit:
Dependencies: Stopgaps:

Status badges

Description

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:

Change History (3)

comment:1 Changed 8 years ago by vbraun_spam

  • Milestone changed from sage-6.1 to sage-6.2

comment:2 Changed 8 years ago by vbraun_spam

  • Milestone changed from sage-6.2 to sage-6.3

comment:3 Changed 7 years ago by vbraun_spam

  • Milestone changed from sage-6.3 to sage-6.4
Note: See TracTickets for help on using tickets.