> I think that this is better since (even though in general the SAT problem
> is know to be NP-hard) in practice a SAT solver is usually more efficient
> than checking one truth table against the other.
>
> [There are some real-world applications of SAT solvers. For example, one
> that I've found very impresive is the use of a SAT Solver to check the
> dependencies among packages in a Debian distribution to decide if a package
> can be installed, developed as part of the Edos Project
> See the paper by Dicosmo et al.
> http://gallium.inria.fr/~xleroy/publi/edos-frcss06.pdf
>
> You can see it in action at http://edos.debian.net/]
+1 for an interface to MiniSat, I'd use it for crypto where it received some
attention lately in cryptanalysis. Note that you could also convert the CNF
to algebraic normal form and use a Gröbner basis algorithm in the boolean
polynomial ring (i.e. PolyBoRi). For some benchmark SAT problems PolyBoRi is
as good as SAT solvers IIRC.
> El Monday 14 July 2008 19:59:06 Chris Gorecki escribió:
> > sage: a = propcalc.formula('a | (b&c)')
> > sage: b = propcalc.formula('(x&y) | z')
> > sage: a.equivlant(b)
> > True
Btw. shouldn't that be
sage: a == b
?
--
name: Martin Albrecht
_pgp: http://pgp.mit.edu:11371/pks/lookup?op=get&search=0x8EF0DC99
_www: http://www.informatik.uni-bremen.de/~malb
_jab: [EMAIL PROTECTED]
--~--~---------~--~----~------------~-------~--~----~
To post to this group, send email to [email protected]
To unsubscribe from this group, send email to [EMAIL PROTECTED]
For more options, visit this group at http://groups.google.com/group/sage-devel
URLs: http://www.sagemath.org
-~----------~----~----~----~------~----~------~--~---
