I agree on point 2. An empty set of clauses WILL entail a tautology. So I
guess you could just simplify the input and if it comes out to be True,
return True, else False.
About point 3, what is the time-complexity of the algorithm that you
propose? Also note how the 'disjuncts' function(for eg) works-
>>> f = And(a, Or(b, c), Not(Or(a, b)))
>>> disjuncts(f)
frozenset([And(Not(a), Not(b), Or(b, c), a)])
>>> disjuncts(to_dnf(f))
frozenset([And(Not(a), Not(b), a, b), And(Not(a), Not(b), a, c)])
You may want to do an amortized analysis of your implementation and check,
because if I get your point right, you would probably want the second
output in the case shown above (for which you will have to do the heavy
to_dnf anyways).
About point 1, I do agree A U {B} being satisfiable does not mean
entailment, since there may be models of A not satisfying B. @asmeurer, am
I missing something here?
On Friday, January 24, 2014 1:05:18 PM UTC+5:30, Soumya Biswas wrote:
>
> 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.
