other.davis_putnam_logemann_loveland
====================================

.. py:module:: other.davis_putnam_logemann_loveland

.. autoapi-nested-parse::

   Davis-Putnam-Logemann-Loveland (DPLL) algorithm is a complete, backtracking-based
   search algorithm for deciding the satisfiability of propositional logic formulae in
   conjunctive normal form, i.e, for solving the Conjunctive Normal Form SATisfiability
   (CNF-SAT) problem.

   For more information about the algorithm: https://en.wikipedia.org/wiki/DPLL_algorithm



Attributes
----------

.. autoapisummary::

   other.davis_putnam_logemann_loveland.formula


Classes
-------

.. autoapisummary::

   other.davis_putnam_logemann_loveland.Clause
   other.davis_putnam_logemann_loveland.Formula


Functions
---------

.. autoapisummary::

   other.davis_putnam_logemann_loveland.dpll_algorithm
   other.davis_putnam_logemann_loveland.find_pure_symbols
   other.davis_putnam_logemann_loveland.find_unit_clauses
   other.davis_putnam_logemann_loveland.generate_clause
   other.davis_putnam_logemann_loveland.generate_formula
   other.davis_putnam_logemann_loveland.generate_parameters


Module Contents
---------------

.. py:class:: Clause(literals: list[str])

   | A clause represented in Conjunctive Normal Form.
   | A clause is a set of literals, either complemented or otherwise.

   For example:
       * {A1, A2, A3'} is the clause (A1 v A2 v A3')
       * {A5', A2', A1} is the clause (A5' v A2' v A1)

   Create model

   >>> clause = Clause(["A1", "A2'", "A3"])
   >>> clause.evaluate({"A1": True})
   True


   .. py:method:: __len__() -> int

      To print a clause as in Conjunctive Normal Form.

      >>> len(Clause([]))
      0
      >>> len(Clause(["A1", "A2'", "A3"]))
      3



   .. py:method:: __str__() -> str

      To print a clause as in Conjunctive Normal Form.

      >>> str(Clause(["A1", "A2'", "A3"]))
      "{A1 , A2' , A3}"



   .. py:method:: assign(model: dict[str, bool | None]) -> None

      Assign values to literals of the clause as given by model.



   .. py:method:: evaluate(model: dict[str, bool | None]) -> bool | None

      Evaluates the clause with the assignments in model.

      This has the following steps:
        1. Return ``True`` if both a literal and its complement exist in the clause.
        2. Return ``True`` if a single literal has the assignment ``True``.
        3. Return ``None`` (unable to complete evaluation)
           if a literal has no assignment.
        4. Compute disjunction of all values assigned in clause.



   .. py:attribute:: literals
      :type:  dict[str, bool | None]


.. py:class:: Formula(clauses: collections.abc.Iterable[Clause])

   | A formula represented in Conjunctive Normal Form.
   | A formula is a set of clauses.
   | For example,
   |   {{A1, A2, A3'}, {A5', A2', A1}} is ((A1 v A2 v A3') and (A5' v A2' v A1))


   .. py:method:: __str__() -> str

      To print a formula as in Conjunctive Normal Form.

      >>> str(Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])]))
      "{{A1 , A2' , A3} , {A5' , A2' , A1}}"



   .. py:attribute:: clauses


.. py:function:: dpll_algorithm(clauses: list[Clause], symbols: list[str], model: dict[str, bool | None]) -> tuple[bool | None, dict[str, bool | None] | None]

   Returns the model if the formula is satisfiable, else ``None``

   This has the following steps:
     1. If every clause in clauses is ``True``, return ``True``.
     2. If some clause in clauses is ``False``, return ``False``.
     3. Find pure symbols.
     4. Find unit symbols.

   >>> formula = Formula([Clause(["A4", "A3", "A5'", "A1", "A3'"]), Clause(["A4"])])
   >>> clauses, symbols = generate_parameters(formula)
   >>> soln, model = dpll_algorithm(clauses, symbols, {})
   >>> soln
   True
   >>> model
   {'A4': True}


.. py:function:: find_pure_symbols(clauses: list[Clause], symbols: list[str], model: dict[str, bool | None]) -> tuple[list[str], dict[str, bool | None]]

   | Return pure symbols and their values to satisfy clause.
   | Pure symbols are symbols in a formula that exist only in one form,
   | either complemented or otherwise.
   | For example,
   |   {{A4 , A3 , A5' , A1 , A3'} , {A4} , {A3}} has pure symbols A4, A5' and A1.

   This has the following steps:
     1. Ignore clauses that have already evaluated to be ``True``.
     2. Find symbols that occur only in one form in the rest of the clauses.
     3. Assign value ``True`` or ``False`` depending on whether the symbols occurs
        in normal or complemented form respectively.

   >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])
   >>> clauses, symbols = generate_parameters(formula)
   >>> pure_symbols, values = find_pure_symbols(clauses, symbols, {})
   >>> pure_symbols
   ['A1', 'A2', 'A3', 'A5']
   >>> values
   {'A1': True, 'A2': False, 'A3': True, 'A5': False}


.. py:function:: find_unit_clauses(clauses: list[Clause], model: dict[str, bool | None]) -> tuple[list[str], dict[str, bool | None]]

   Returns the unit symbols and their values to satisfy clause.

   Unit symbols are symbols in a formula that are:
     - Either the only symbol in a clause
     - Or all other literals in that clause have been assigned ``False``

   This has the following steps:
     1. Find symbols that are the only occurrences in a clause.
     2. Find symbols in a clause where all other literals are assigned ``False``.
     3. Assign ``True`` or ``False`` depending on whether the symbols occurs in
        normal or complemented form respectively.

   >>> clause1 = Clause(["A4", "A3", "A5'", "A1", "A3'"])
   >>> clause2 = Clause(["A4"])
   >>> clause3 = Clause(["A3"])
   >>> clauses, symbols = generate_parameters(Formula([clause1, clause2, clause3]))
   >>> unit_clauses, values = find_unit_clauses(clauses, {})
   >>> unit_clauses
   ['A4', 'A3']
   >>> values
   {'A4': True, 'A3': True}


.. py:function:: generate_clause() -> Clause

   | Randomly generate a clause.
   | All literals have the name Ax, where x is an integer from ``1`` to ``5``.


.. py:function:: generate_formula() -> Formula

   Randomly generate a formula.


.. py:function:: generate_parameters(formula: Formula) -> tuple[list[Clause], list[str]]

   | Return the clauses and symbols from a formula.
   | A symbol is the uncomplemented form of a literal.

   For example,
     * Symbol of A3 is A3.
     * Symbol of A5' is A5.

   >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])
   >>> clauses, symbols = generate_parameters(formula)
   >>> clauses_list = [str(i) for i in clauses]
   >>> clauses_list
   ["{A1 , A2' , A3}", "{A5' , A2' , A1}"]
   >>> symbols
   ['A1', 'A2', 'A3', 'A5']


.. py:data:: formula