def satisfiable(expr, algorithm="dpll2"):
    """
    Check satisfiability of a propositional sentence.
    Returns a model when it succeeds

    Examples:

    >>> from sympy.abc import A, B
    >>> from sympy.logic.inference import satisfiable
    >>> satisfiable(A & ~B)
    {A: True, B: False}
    >>> satisfiable(A & ~A)
    False

    """
    expr = to_cnf(expr)
    if algorithm == "dpll":
        from sympy.logic.algorithms.dpll import dpll_satisfiable

        return dpll_satisfiable(expr)
    elif algorithm == "dpll2":
        from sympy.logic.algorithms.dpll2 import dpll_satisfiable

        return dpll_satisfiable(expr)
    raise NotImplementedError

def satisfiable(expr, algorithm="dpll2", all_models=False):
    """
    Check satisfiability of a propositional sentence.
    Returns a model when it succeeds.
    Returns {true: true} for trivially true expressions.

    On setting all_models to True, if given expr is satisfiable then
    returns a generator of models. However, if expr is unsatisfiable
    then returns a generator containing the single element False.

    Examples
    ========

    >>> from sympy.abc import A, B
    >>> from sympy.logic.inference import satisfiable
    >>> satisfiable(A & ~B)
    {A: True, B: False}
    >>> satisfiable(A & ~A)
    False
    >>> satisfiable(True)
    {True: True}
    >>> next(satisfiable(A & ~A, all_models=True))
    False
    >>> models = satisfiable((A >> B) & B, all_models=True)
    >>> next(models)
    {A: False, B: True}
    >>> next(models)
    {A: True, B: True}
    >>> def use_models(models):
    ...     for model in models:
    ...         if model:
    ...             # Do something with the model.
    ...             print(model)
    ...         else:
    ...             # Given expr is unsatisfiable.
    ...             print("UNSAT")
    >>> use_models(satisfiable(A >> ~A, all_models=True))
    {A: False}
    >>> use_models(satisfiable(A ^ A, all_models=True))
    UNSAT

    """
    expr = to_cnf(expr)
    if algorithm == "dpll":
        from sympy.logic.algorithms.dpll import dpll_satisfiable

        return dpll_satisfiable(expr)
    elif algorithm == "dpll2":
        from sympy.logic.algorithms.dpll2 import dpll_satisfiable

        return dpll_satisfiable(expr, all_models)
    raise NotImplementedError

def test_dpll_satisfiable():
    A, B, C = symbols('A,B,C')
    assert dpll_satisfiable( A & ~A ) == False
    assert dpll_satisfiable( A & ~B ) == {A: True, B: False}
    assert dpll_satisfiable( A | B ) in ({A: True}, {B: True}, {A: True, B: True})
    assert dpll_satisfiable( (~A | B) & (~B | A) ) in ({A: True, B: True}, {A: False, B:False})
    assert dpll_satisfiable( (A | B) & (~B | C) ) in ({A: True, B: False}, {A: True, C:True})
    assert dpll_satisfiable( A & B & C  ) == {A: True, B: True, C: True}
    assert dpll_satisfiable( (A | B) & (A >> B) ) == {B: True}
    assert dpll_satisfiable( Equivalent(A, B) & A ) == {A: True, B: True}
    assert dpll_satisfiable( Equivalent(A, B) & ~A ) == {A: False, B: False}

def satisfiable(expr, algorithm="dpll"):
    """Check satisfiability of a propositional sentence.
    Returns a model when it succeeds

    Examples
    >>> from sympy import symbols
    >>> A, B = symbols('AB')
    >>> satisfiable(A & ~B)
    {A: True, B: False}
    >>> satisfiable(A & ~A)
    False
    """
    expr = to_cnf(expr)
    if algorithm == "dpll":
        from sympy.logic.algorithms.dpll import dpll_satisfiable
        return dpll_satisfiable(expr)
    raise NotImplementedError

def main():
    with open(sys.argv[1]) as cnf_file:
        cnf = load(cnf_file.read())
    result = dpll_satisfiable(cnf)
    print(result)
    return 0

def test_f1():
    assert bool(dpll_satisfiable(load(f1)))

def test_f4():
    # re-enable this when dpll is efficient
    skip('Takes too much time')
    assert not bool(dpll_satisfiable(load(f4)))

def test_f3():
    assert bool(dpll_satisfiable(load(f3)))

def test_f2():
    assert bool(dpll_satisfiable(load(f2)))

def test_f4():
    assert not bool(dpll_satisfiable(load(f4)))

def test_f5():
    assert bool(dpll_satisfiable(load(f5)))