On Jul 15, 2008, at 11:34 AM, Chris Gorecki wrote:
> Thank you all for your responses.
>
>> "Wrap minisat"
>
> The code already implements a satformat output method which can be
> read directly by MiniSat, so this is the route I will most likely be
> taking. This would have the added advantage o
Thank you all for your responses.
>"Wrap minisat"
The code already implements a satformat output method which can be
read directly by MiniSat, so this is the route I will most likely be
taking. This would have the added advantage of fully incorporating
MiniSat into Sage.
>> Btw. shouldn't that
>
> Btw. shouldn't that be
>
> sage: a == b
>
not for *formulas*, since say also involve the syntax.
In terms of polynomials
(a+b)*c==a*b+b*c
But they are different formulas.
Anyway: I recommend to
multiply the the prop. calc. formulas by converting them to
Boolean polynomials (in the quot
> 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
Hi Chris and others,
Certainly there are betters ways to do that.
For this and similar problems in propositional logic,
I would suggest to wrap a SAT solver.
(see the article on wikipedia)
http://en.wikipedia.org/wiki/SAT_solver##Algorithms_for_solving_SAT
and the ticket #418
"Wrap minisat"
ht
On Jul 14, 3:59 pm, Chris Gorecki <[EMAIL PROTECTED]> wrote:
> Hi All,
>
> I'm currently trying to implement a function for the propositional
> calculus package that would determine if two statements are logically
> equivalent. The usage would be something along the lines of:
>
> sage: a = prop
