Opened 9 years ago

Last modified 8 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 9 years ago by For batch modifications

Milestone: sage-6.1sage-6.2

comment:2 Changed 9 years ago by For batch modifications

Milestone: sage-6.2sage-6.3

comment:3 Changed 8 years ago by For batch modifications

Milestone: sage-6.3sage-6.4
Note: See TracTickets for help on using tickets.