Hello
There are a couple of things present in the Logic module that I would like
to discuss:
1. Ask Function in PropKB:
If KB 'A' entails formula 'B' then A U {~B} is unsatisfiable. However the
current code seems to check if A U {B} is satisfiable. To the best of my
understanding, this will give the right answer in many case, but not all.
2. Ask Function on a PropKB with no clauses:
The function returns False if there are no clauses. Theoretically, an empty
clause is unsatisfiable but empty clause set is valid. Hence, it is
satisfiable in all interpretations. So it only entails formulas that are
satisfiable in all interpretation i.e. valid. So shouldn't an empty KB
entail a tautology?
3. DNF Satisfiability:
As discussed before, the time taken by to_cnf is actually more than the
time taken by the SAT solver. A relatively quick and dirty way to decide
whether the formula resembles CNF or DNF can be to compare the number of
conjuncts and disjuncts present in the formula. This seems to be giving
reasonable results. So, I want to change the code to do this: If more
conjunctive then dpll, else dnf sat. DNF Satisfiability seems to be a
linear problem and would be easier to compute. Is this okay?
I am done with the code for the above issues and will send a PR once
someone confirms my ideas.
--
You received this message because you are subscribed to the Google Groups
"sympy" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at http://groups.google.com/group/sympy.
For more options, visit https://groups.google.com/groups/opt_out.
