aima/logic.py
def dpll(clauses, symbols, model):
    "See if the clauses are true in a partial model."
    unknown_clauses = [] ## clauses with an unknown truth value
    for c in clauses:
        val =  pl_true(c, model)
        if val == False:
            return False
        if val != True:
            unknown_clauses.append(c)
    if not unknown_clauses:
        return model
    P, value = find_pure_symbol(symbols, unknown_clauses)
    if P:
        return dpll(clauses, removeall(P, symbols), extend(model, P, value))
    P, value = find_unit_clause(clauses, model)
    if P:
        return dpll(clauses, removeall(P, symbols), extend(model, P, value))
    P, symbols = symbols[0], symbols[1:]
    return (dpll(clauses, symbols, extend(model, P, True)) or
            dpll(clauses, symbols, extend(model, P, False)))
def dpll(clauses, symbols, model):
    "See if the clauses are true in a partial model."
    unknown_clauses = [] ## clauses with an unknown truth value
    for c in clauses:
        val =  pl_true(c, model)
        if val == False:
            return False
        if val != True:
            unknown_clauses.append(c)
    if not unknown_clauses:
        return model
    P, value = find_pure_symbol(symbols, unknown_clauses)
    if P:
        return dpll(clauses, removeall(P, symbols), extend(model, P, value))
    P, value = find_unit_clause(clauses, model)
    if P:
        return dpll(clauses, removeall(P, symbols), extend(model, P, value))
    P, symbols = symbols[0], symbols[1:]
    return (dpll(clauses, symbols, extend(model, P, True)) or
            dpll(clauses, symbols, extend(model, P, False)))
def dpll ( clauses , symbols , model ) : unknown_clauses = [ ] ## clauses with an unknown truth value for c in clauses : val = pl_true ( c , model ) if val == False : return False if val != True : unknown_clauses . append ( c ) if not unknown_clauses : return model P , value = find_pure_symbol ( symbols , unknown_clauses ) if P : return dpll ( clauses , removeall ( P , symbols ) , extend ( model , P , value ) ) P , value = find_unit_clause ( clauses , model ) if P : return dpll ( clauses , removeall ( P , symbols ) , extend ( model , P , value ) ) P , symbols = symbols [ 0 ] , symbols [ 1 : ] return ( dpll ( clauses , symbols , extend ( model , P , True ) ) or dpll ( clauses , symbols , extend ( model , P , False ) ) )
See if the clauses are true in a partial model.
See if the clauses are true in a partial model .