Opened 6 years ago

Last modified 5 years ago

#15680 new enhancement

Using SAT solver module from Symbolic Logic module

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

Description

It seems (but I am not entirely sure) that currently the Symbolic Logic module does not (optionally) use the SAT solver module for the is_satisfiable() method. As this can make this method more efficient, it can be a useful addition. (And allow returning a satisfying instance of the variables.)

(N.B.: Both modules seem to have a method outputting DIMACS format.)

Links:

Change History (4)

comment:1 Changed 6 years ago by ncohen

  • Cc malb added

comment:2 Changed 6 years ago by vbraun_spam

  • Milestone changed from sage-6.1 to sage-6.2

comment:3 Changed 5 years ago by vbraun_spam

  • Milestone changed from sage-6.2 to sage-6.3

comment:4 Changed 5 years ago by vbraun_spam

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