fiind_unit_clause function used by dpll_satisfiable in logic.py has a missing case


To reproduce the problem try running the following script:

import logic

print logic.dpll_satisfiable(logic.expr("A & ~B & C & (A | ~D) & (~E | ~D) & (C 
| ~D) & (~A | ~F) & (E | ~F) & (~D | ~F) & (B | ~C | D) & (A | ~E | F) & (~A | 
E | D)"))

It will produce "False" as an answer while there actually exists a model i.e. 
the expected output should be:

{B: False, C: True, A: True, F: False, D: True, E: False}

The problem occurs in v193 of logic.py from SVN that arrives with v201 of the 
overall package.

The problem is due to a missed case in find_unit_clause function in logic.py. 
When searching for new unit clauses after assigning True to A, False to B, True 
to C and False to F, the algorithm mistakenly assigns False to D due to clause 
(A | ~D). The problem is due to missing check on whether the clause is already 
true or not. A possible fixed version of the find_unit_clause function is below:

def find_unit_clause(clauses, model):
    """A unit clause has only 1 variable that is not bound in the model.
    >>> find_unit_clause([A|B|C, B|~C, A|~B], {A:True})
    (B, False)
    """
    for clause in clauses:
        num_not_in_model = 0
        clause_true=False
        for literal in disjuncts(clause):
            sym = literal_symbol(literal)
            if sym not in model:
                num_not_in_model += 1
                P, value = sym, (literal.op != '~')
            else:
                clause_true = clause_true | (model[sym] == (literal.op != '~' ))
        if ((num_not_in_model == 1) and not(clause_true)):
            return P, value
    return None, None

Original issue reported on code.google.com by juhan.er...@gmail.com on 10 Dec 2012 at 10:34

ekr- / aima-python

fiind_unit_clause function used by dpll_satisfiable in logic.py has a missing case #35