You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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 [email protected] on 10 Dec 2012 at 10:34
The text was updated successfully, but these errors were encountered:
Original issue reported on code.google.com by
[email protected]
on 10 Dec 2012 at 10:34The text was updated successfully, but these errors were encountered: