Initialisation du repository de Beta

venv/lib/python3.12/site-packages/sympy/logic/algorithms/dpll.py

@@ -0,0 +1,308 @@
+"""Implementation of DPLL algorithm
+
+Further improvements: eliminate calls to pl_true, implement branching rules,
+efficient unit propagation.
+
+References:
+  - https://en.wikipedia.org/wiki/DPLL_algorithm
+  - https://www.researchgate.net/publication/242384772_Implementations_of_the_DPLL_Algorithm
+"""
+
+from sympy.core.sorting import default_sort_key
+from sympy.logic.boolalg import Or, Not, conjuncts, disjuncts, to_cnf, \
+    to_int_repr, _find_predicates
+from sympy.assumptions.cnf import CNF
+from sympy.logic.inference import pl_true, literal_symbol
+
+
+def dpll_satisfiable(expr):
+    """
+    Check satisfiability of a propositional sentence.
+    It returns a model rather than True when it succeeds
+
+    >>> from sympy.abc import A, B
+    >>> from sympy.logic.algorithms.dpll import dpll_satisfiable
+    >>> dpll_satisfiable(A & ~B)
+    {A: True, B: False}
+    >>> dpll_satisfiable(A & ~A)
+    False
+
+    """
+    if not isinstance(expr, CNF):
+        clauses = conjuncts(to_cnf(expr))
+    else:
+        clauses = expr.clauses
+    if False in clauses:
+        return False
+    symbols = sorted(_find_predicates(expr), key=default_sort_key)
+    symbols_int_repr = set(range(1, len(symbols) + 1))
+    clauses_int_repr = to_int_repr(clauses, symbols)
+    result = dpll_int_repr(clauses_int_repr, symbols_int_repr, {})
+    if not result:
+        return result
+    output = {}
+    for key in result:
+        output.update({symbols[key - 1]: result[key]})
+    return output
+
+
+def dpll(clauses, symbols, model):
+    """
+    Compute satisfiability in a partial model.
+    Clauses is an array of conjuncts.
+
+    >>> from sympy.abc import A, B, D
+    >>> from sympy.logic.algorithms.dpll import dpll
+    >>> dpll([A, B, D], [A, B], {D: False})
+    False
+
+    """
+    # compute DP kernel
+    P, value = find_unit_clause(clauses, model)
+    while P:
+        model.update({P: value})
+        symbols.remove(P)
+        if not value:
+            P = ~P
+        clauses = unit_propagate(clauses, P)
+        P, value = find_unit_clause(clauses, model)
+    P, value = find_pure_symbol(symbols, clauses)
+    while P:
+        model.update({P: value})
+        symbols.remove(P)
+        if not value:
+            P = ~P
+        clauses = unit_propagate(clauses, P)
+        P, value = find_pure_symbol(symbols, clauses)
+    # end DP kernel
+    unknown_clauses = []
+    for c in clauses:
+        val = pl_true(c, model)
+        if val is False:
+            return False
+        if val is not True:
+            unknown_clauses.append(c)
+    if not unknown_clauses:
+        return model
+    if not clauses:
+        return model
+    P = symbols.pop()
+    model_copy = model.copy()
+    model.update({P: True})
+    model_copy.update({P: False})
+    symbols_copy = symbols[:]
+    return (dpll(unit_propagate(unknown_clauses, P), symbols, model) or
+            dpll(unit_propagate(unknown_clauses, Not(P)), symbols_copy, model_copy))
+
+
+def dpll_int_repr(clauses, symbols, model):
+    """
+    Compute satisfiability in a partial model.
+    Arguments are expected to be in integer representation
+
+    >>> from sympy.logic.algorithms.dpll import dpll_int_repr
+    >>> dpll_int_repr([{1}, {2}, {3}], {1, 2}, {3: False})
+    False
+
+    """
+    # compute DP kernel
+    P, value = find_unit_clause_int_repr(clauses, model)
+    while P:
+        model.update({P: value})
+        symbols.remove(P)
+        if not value:
+            P = -P
+        clauses = unit_propagate_int_repr(clauses, P)
+        P, value = find_unit_clause_int_repr(clauses, model)
+    P, value = find_pure_symbol_int_repr(symbols, clauses)
+    while P:
+        model.update({P: value})
+        symbols.remove(P)
+        if not value:
+            P = -P
+        clauses = unit_propagate_int_repr(clauses, P)
+        P, value = find_pure_symbol_int_repr(symbols, clauses)
+    # end DP kernel
+    unknown_clauses = []
+    for c in clauses:
+        val = pl_true_int_repr(c, model)
+        if val is False:
+            return False
+        if val is not True:
+            unknown_clauses.append(c)
+    if not unknown_clauses:
+        return model
+    P = symbols.pop()
+    model_copy = model.copy()
+    model.update({P: True})
+    model_copy.update({P: False})
+    symbols_copy = symbols.copy()
+    return (dpll_int_repr(unit_propagate_int_repr(unknown_clauses, P), symbols, model) or
+            dpll_int_repr(unit_propagate_int_repr(unknown_clauses, -P), symbols_copy, model_copy))
+
+### helper methods for DPLL
+
+
+def pl_true_int_repr(clause, model={}):
+    """
+    Lightweight version of pl_true.
+    Argument clause represents the set of args of an Or clause. This is used
+    inside dpll_int_repr, it is not meant to be used directly.
+
+    >>> from sympy.logic.algorithms.dpll import pl_true_int_repr
+    >>> pl_true_int_repr({1, 2}, {1: False})
+    >>> pl_true_int_repr({1, 2}, {1: False, 2: False})
+    False
+
+    """
+    result = False
+    for lit in clause:
+        if lit < 0:
+            p = model.get(-lit)
+            if p is not None:
+                p = not p
+        else:
+            p = model.get(lit)
+        if p is True:
+            return True
+        elif p is None:
+            result = None
+    return result
+
+
+def unit_propagate(clauses, symbol):
+    """
+    Returns an equivalent set of clauses
+    If a set of clauses contains the unit clause l, the other clauses are
+    simplified by the application of the two following rules:
+
+      1. every clause containing l is removed
+      2. in every clause that contains ~l this literal is deleted
+
+    Arguments are expected to be in CNF.
+
+    >>> from sympy.abc import A, B, D
+    >>> from sympy.logic.algorithms.dpll import unit_propagate
+    >>> unit_propagate([A | B, D | ~B, B], B)
+    [D, B]
+
+    """
+    output = []
+    for c in clauses:
+        if c.func != Or:
+            output.append(c)
+            continue
+        for arg in c.args:
+            if arg == ~symbol:
+                output.append(Or(*[x for x in c.args if x != ~symbol]))
+                break
+            if arg == symbol:
+                break
+        else:
+            output.append(c)
+    return output
+
+
+def unit_propagate_int_repr(clauses, s):
+    """
+    Same as unit_propagate, but arguments are expected to be in integer
+    representation
+
+    >>> from sympy.logic.algorithms.dpll import unit_propagate_int_repr
+    >>> unit_propagate_int_repr([{1, 2}, {3, -2}, {2}], 2)
+    [{3}]
+
+    """
+    negated = {-s}
+    return [clause - negated for clause in clauses if s not in clause]
+
+
+def find_pure_symbol(symbols, unknown_clauses):
+    """
+    Find a symbol and its value if it appears only as a positive literal
+    (or only as a negative) in clauses.
+
+    >>> from sympy.abc import A, B, D
+    >>> from sympy.logic.algorithms.dpll import find_pure_symbol
+    >>> find_pure_symbol([A, B, D], [A|~B,~B|~D,D|A])
+    (A, True)
+
+    """
+    for sym in symbols:
+        found_pos, found_neg = False, False
+        for c in unknown_clauses:
+            if not found_pos and sym in disjuncts(c):
+                found_pos = True
+            if not found_neg and Not(sym) in disjuncts(c):
+                found_neg = True
+        if found_pos != found_neg:
+            return sym, found_pos
+    return None, None
+
+
+def find_pure_symbol_int_repr(symbols, unknown_clauses):
+    """
+    Same as find_pure_symbol, but arguments are expected
+    to be in integer representation
+
+    >>> from sympy.logic.algorithms.dpll import find_pure_symbol_int_repr
+    >>> find_pure_symbol_int_repr({1,2,3},
+    ...     [{1, -2}, {-2, -3}, {3, 1}])
+    (1, True)
+
+    """
+    all_symbols = set().union(*unknown_clauses)
+    found_pos = all_symbols.intersection(symbols)
+    found_neg = all_symbols.intersection([-s for s in symbols])
+    for p in found_pos:
+        if -p not in found_neg:
+            return p, True
+    for p in found_neg:
+        if -p not in found_pos:
+            return -p, False
+    return None, None
+
+
+def find_unit_clause(clauses, model):
+    """
+    A unit clause has only 1 variable that is not bound in the model.
+
+    >>> from sympy.abc import A, B, D
+    >>> from sympy.logic.algorithms.dpll import find_unit_clause
+    >>> find_unit_clause([A | B | D, B | ~D, A | ~B], {A:True})
+    (B, False)
+
+    """
+    for clause in clauses:
+        num_not_in_model = 0
+        for literal in disjuncts(clause):
+            sym = literal_symbol(literal)
+            if sym not in model:
+                num_not_in_model += 1
+                P, value = sym, not isinstance(literal, Not)
+        if num_not_in_model == 1:
+            return P, value
+    return None, None
+
+
+def find_unit_clause_int_repr(clauses, model):
+    """
+    Same as find_unit_clause, but arguments are expected to be in
+    integer representation.
+
+    >>> from sympy.logic.algorithms.dpll import find_unit_clause_int_repr
+    >>> find_unit_clause_int_repr([{1, 2, 3},
+    ...     {2, -3}, {1, -2}], {1: True})
+    (2, False)
+
+    """
+    bound = set(model) | {-sym for sym in model}
+    for clause in clauses:
+        unbound = clause - bound
+        if len(unbound) == 1:
+            p = unbound.pop()
+            if p < 0:
+                return -p, False
+            else:
+                return p, True
+    return None, None