@Aaron, I don't think getting rid of PropKB is a good idea. But what IS
needed is to make sure its foolproof. A PropKB(propositional knowledge
base) is essentially a tool to check whether a set of logic expressions 'A'
_entail_ a certain expression 'B'. Essentially, whether ALL models of A are
models of B. This is a nice tool to use for deductions. Currently, it calls
the dpll algo, but I guess wrongly. So that should be fixed.
About satisfiable(), and especially for the assumptions system, may I
suggest looking at other, lighter SAT solvers like MiniSAT? We may have to
confirm the soundness and completeness, but thats still an avenue to
explore.
@Soumya, I would suggest you send a PR with what modifications you propose,
and we take it from there.
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.
