The function dpll_satisfiable in logic.py requires arguments to be expr-s.

[GoogleCodeExporter]

* What are the steps to reproduce the problem?

It is often quite convenient to manipulate propositional sentences in string 
format
and then pass them to dpll_satisfiable to be solved.
If you pass a string argument to dpll_satisfiable, it sometimes works correctly 
(in the cases when no choice is required), but other times gives an obscure 
"out of index" error.

* What is the expected output? What do you see instead?

Running:
>>> import logic
>>> logic.dpll_satisfiable("A")
{A: True}

Expected result would be {A: True}

But then the following behaviour:

>>> logic.dpll_satisfiable("A | B")
Traceback from previous calls
 ...
    P, symbols = symbols[0], symbols[1:]
IndexError: list index out of range

I would expect to get either
{A: True}
or an error that the type of the argument should be Expr.

* What version of the product are you using? On what operating system?

The problem is in r202 (and earlier revisions) from the repository.


* Please provide any additional information below.

The debugging can be made much simpler by adding the following line to logic.py:

@@ -643,6 +643,7 @@
     >>> dpll_satisfiable(P&~P)
     False
     """
+    assert isinstance(s, Expr), "The argument 's' must be an instance of the 
Expr type. Use logic.expr(string) to convert a string to Expr instance."
     clauses = conjuncts(to_cnf(s))
     symbols = prop_symbols(s)
     return dpll(clauses, symbols, {})


The code in this project is wonderful for learning and teaching purposes and 
adding clutter is generally not a good idea. In this case the little additional 
clutter is justified to save time in debugging and ease understanding.

Original issue reported on code.google.com by juhan.er...@gmail.com on 7 Dec 2013 at 1:16