cnf.py

cnf.py

Constructors and functions for sentences in conjunctive normal form (Cnf).

Clause

Bases: frozenset[Lit]

Clause is a subclass of frozenset[Lit].

Source code in normal_form/cnf.py

class Clause(frozenset[Lit]):  # pylint: disable=too-few-public-methods
    """`Clause` is a subclass of `frozenset[Lit]`."""
    def __repr__(self) -> str:
        sorted_lit_values: Generator[str, None, None] = (str(lit.value)
                                                         for lit in sorted(self))
        return f"Clause({{{', '.join(sorted_lit_values)}}})"

Cnf

Bases: frozenset[Clause]

Cnf is a subclass of frozenset[Clause].

Source code in normal_form/cnf.py

class Cnf(frozenset[Clause]):  # pylint: disable=too-few-public-methods
    """`Cnf` is a subclass of `frozenset[Clause]`."""

    def __str__(self) -> str:
        """Pretty print a Cnf after sorting its sorted clause tuples."""
        sorted_clause_values: Iterator[str] = map(str, sorted(self))
        return f"Cnf({{{', '.join(sorted_clause_values)}}})"

__str__()

Pretty print a Cnf after sorting its sorted clause tuples.

Source code in normal_form/cnf.py

def __str__(self) -> str:
    """Pretty print a Cnf after sorting its sorted clause tuples."""
    sorted_clause_values: Iterator[str] = map(str, sorted(self))
    return f"Cnf({{{', '.join(sorted_clause_values)}}})"

absolute_value(literal)

Unnegated form of a Lit.

This function is idempotent.

Parameters:

Name	Type	Description	Default
literal		obj:Lit): a Lit formed from a nonzero integer.	required

Return

Check that literal is not of type Bool and then return the absolute value of literal. If it is of type Bool, then return literal as is.

Source code in normal_form/cnf.py

def absolute_value(literal: Lit) -> Lit:
    """Unnegated form of a Lit.

    This function is idempotent.

    Args:
       literal (:obj:`Lit`): a Lit formed from a nonzero integer.

    Return:
       Check that ``literal`` is not of type Bool and then return the absolute value of
          ``literal``. If it is of type Bool, then return ``literal`` as is.
    """
    if isinstance(literal.value, Bool):
        return lit(Bool.TRUE)
    return lit(abs(literal.value))

assign(cnf_instance, assignment)

Assign Bool values to Variables if present in Cnf.

For each Variable (key) in assignment, replace the Variable and its negation in cnf_instance using the Bool (value) in assignment. The final output is always tautologically reduced. This function is idempotent.

Parameters:

Name	Type	Description	Default
cnf_instance		obj:Cnf)	required
assignment		obj:Assignment): a dict with keys being Variables to be replaced and values being Bools that the Variables are to be assigned to. The assignment dict need not be complete and can be partial.	required

Edge case

An empty assignment dict results in cnf_instance simply getting tautologically reduced.

Return

Tautologically-reduced Cnf formed by replacing every key in the assignment dict (and those keys' negations) by corresponding Bool values.

Source code in normal_form/cnf.py

def assign(cnf_instance: Cnf, assignment: Assignment) -> Cnf:
    """Assign Bool values to Variables if present in Cnf.

    For each Variable (key) in ``assignment``, replace the Variable and its negation in
    ``cnf_instance`` using the Bool (value) in ``assignment``. The final output is always
    tautologically reduced. This function is idempotent.

    Args:
       cnf_instance (:obj:`Cnf`)
       assignment (:obj:`Assignment`): a dict with keys being Variables to be replaced and
          values being Bools that the Variables are to be assigned to.  The ``assignment``
          dict need not be complete and can be partial.

    Edge case:
       An empty assignment dict results in ``cnf_instance`` simply getting tautologically
          reduced.

    Return:
       Tautologically-reduced Cnf formed by replacing every key in the ``assignment`` dict (and
          those keys' negations) by corresponding Bool values.
    """
    for variable_instance, boolean in assignment.items():
        cnf_instance = assign_variable_in_cnf(cnf_instance, variable_instance, boolean)
    return tauto_reduce(cnf_instance)

assign_variable_in_clause(clause_instance, variable_instance, boolean)

Assign Bool value to a Variable if present in Clause.

Replace all instances of variable_instance and its negation in clause_instance with boolean and its negation respectively. Leave all else unchanged. Perform tautological reductions on the Clause before returning results. This function is idempotent.

Parameters:

Name	Type	Description	Default
clause_instance		obj:set[Lit]): an abstract set (set or frozenset) of Lits.	required
variable_instance		obj:Variable)	required
boolean		obj:Bool): either TRUE or FALSE.	required

Return

Tautologically-reduced Clause formed by assigning variable_instance to boolean in clause_instance.

Source code in normal_form/cnf.py

def assign_variable_in_clause(
    clause_instance: Clause, variable_instance: Variable, boolean: Bool
) -> Clause:
    """Assign Bool value to a Variable if present in Clause.

    Replace all instances of ``variable_instance`` and its negation in ``clause_instance`` with
    ``boolean`` and its negation respectively. Leave all else unchanged. Perform tautological
    reductions on the Clause before returning results. This function is idempotent.

    Args:
       clause_instance (:obj:`set[Lit]`): an abstract set (set or frozenset) of Lits.
       variable_instance (:obj:`Variable`)
       boolean (:obj:`Bool`): either ``TRUE`` or ``FALSE``.

    Return:
       Tautologically-reduced Clause formed by assigning ``variable_instance`` to ``boolean``
          in ``clause_instance``.
    """
    assign_variable: Callable[[Lit], Lit]
    assign_variable = ft.partial(
        assign_variable_in_lit, variable_instance=variable_instance, boolean=boolean
    )
    mapped_lits: set[Lit]
    mapped_lits = set(map(assign_variable, clause_instance))

    return tauto_reduce(clause(mapped_lits))

assign_variable_in_cnf(cnf_instance, variable_instance, boolean)

Assign Bool value to a Variable if present in Cnf.

Replace all instances of variable_instance and its negation in cnf_instance with boolean and its negation respectively. Leave all else unchanged. Perform tautological reductions on the Cnf before returning results. This function is idempotent.

Parameters:

Name	Type	Description	Default
cnf_instance		obj:set[set[Lit]]): an abstract set (set or frozenset) of abstract sets of Lits.	required
variable_instance		obj:Variable)	required
boolean		obj:Bool): either TRUE or FALSE.	required

Return

Tautologically-reduced Cnf formed by assigning variable_instance to boolean in cnf_instance.

Source code in normal_form/cnf.py

def assign_variable_in_cnf(
    cnf_instance: Cnf, variable_instance: Variable, boolean: Bool
) -> Cnf:
    """Assign Bool value to a Variable if present in Cnf.

    Replace all instances of ``variable_instance`` and its negation in ``cnf_instance`` with
    ``boolean`` and its negation respectively. Leave all else unchanged. Perform tautological
    reductions on the Cnf before returning results. This function is idempotent.

    Args:
       cnf_instance (:obj:`set[set[Lit]]`): an abstract set (set or frozenset) of abstract sets
          of Lits.
       variable_instance (:obj:`Variable`)
       boolean (:obj:`Bool`): either ``TRUE`` or ``FALSE``.

    Return:
       Tautologically-reduced Cnf formed by assigning ``variable_instance`` to ``boolean`` in
          ``cnf_instance``.
    """
    assign_variable: Callable[[Clause], Clause]
    assign_variable = ft.partial(
        assign_variable_in_clause, variable_instance=variable_instance, boolean=boolean
    )

    mapped_clauses: set[Clause]
    mapped_clauses = set(map(assign_variable, cnf_instance))

    return tauto_reduce(cnf(mapped_clauses))

assign_variable_in_lit(literal, variable_instance, boolean)

Assign Bool value to a Variable if present in Lit.

Replace all instances of variable_instance and its negation with boolean and its negation respectively. Leave all else unchanged. This function is idempotent.

Parameters:

Name	Type	Description	Default
literal		obj:Lit)	required
variable_instance		obj:Variable)	required
boolean		obj:Bool): either TRUE or FALSE.	required

Return

Lit formed by assigning variable_instance to boolean in literal.

Source code in normal_form/cnf.py

def assign_variable_in_lit(
    literal: Lit, variable_instance: Variable, boolean: Bool
) -> Lit:
    """Assign Bool value to a Variable if present in Lit.

    Replace all instances of ``variable_instance`` and its negation with ``boolean`` and its
    negation respectively. Leave all else unchanged. This function is idempotent.

    Args:
       literal (:obj:`Lit`)
       variable_instance (:obj:`Variable`)
       boolean (:obj:`Bool`): either ``TRUE`` or ``FALSE``.

    Return:
       Lit formed by assigning ``variable_instance`` to ``boolean`` in ``literal``.
    """
    if literal.value == variable_instance:
        return lit(boolean)
    if literal.value == - variable_instance:
        return neg(lit(boolean))
    return literal

clause(lit_iterable)

Constructor-function for Clause type.

By definition, a Clause is a nonempty frozenset of Lits. This function is idempotent.

Parameters:

Name	Type	Description	Default
lit_iterable		obj:Iterable[int]): a nonempty iterable of ints, Bools, or Lits.	required

Return

Check that each element in the iterable satisfies axioms for being a Lit and then cast to Clause.

Raises:

Type	Description
ValueError	if lit_iterable is an empty iterable.

Source code in normal_form/cnf.py

def clause(lit_iterable: Iterable[int | Bool | Lit]) -> Clause:
    """Constructor-function for Clause type.

    By definition, a `Clause` is a nonempty frozenset of Lits. This function is idempotent.

    Args:
       lit_iterable (:obj:`Iterable[int]`): a nonempty iterable of ints, Bools, or Lits.

    Return:
       Check that each element in the iterable satisfies axioms for being a Lit and then cast
          to Clause.

    Raises:
       ValueError: if ``lit_iterable`` is an empty iterable.

    """
    head, lit_iterable = mit.spy(lit_iterable)
    if not head:
        raise ValueError(f"Encountered empty input {list(lit_iterable)}.")
    return Clause(frozenset(map(lit, lit_iterable)))

cnf(clause_collection)

Constructor-function for Cnf type.

By definition, a Cnf is a nonempty frozenset of Clauses. This function is idempotent.

Parameters:

Name	Type	Description	Default
clause_collection		obj:Iterable[Iterable[int]]): a nonempty iterable (list, tuple, set, frozenset) of nonempty collections of integers or Bools.	required

Return

Check that each element in the iterable satisfies axioms for being a Clause and then cast to Cnf.

Raises:

Type	Description
ValueError	if clause_collection is an empty iterable.

Source code in normal_form/cnf.py

def cnf(clause_collection: Iterable[Iterable[int | Bool | Lit]]) -> Cnf:
    """Constructor-function for Cnf type.

    By definition, a `Cnf` is a nonempty frozenset of Clauses. This function is idempotent.

    Args:
       clause_collection (:obj:`Iterable[Iterable[int]]`): a nonempty iterable (list,
          tuple, set, frozenset) of nonempty collections of integers or Bools.

    Return:
       Check that each element in the iterable satisfies axioms for being a Clause and
          then cast to Cnf.

    Raises:
       ValueError: if ``clause_collection`` is an empty iterable.
    """
    head, clause_collection = mit.spy(clause_collection)
    if not head:
        raise ValueError(f"Encountered empty input {list(clause_collection)}.")
    return Cnf(frozenset(map(clause, clause_collection)))

lits(cnf_instance)

Return frozenset of all Lits that appear in a Cnf.

Parameters:

Name	Type	Description	Default
cnf_instance		obj:Cnf)	required

Return

A frozenset of all lits that appear in a Cnf.

Source code in normal_form/cnf.py

def lits(cnf_instance: Cnf) -> frozenset[Lit]:
    """Return frozenset of all Lits that appear in a Cnf.

    Args:
       cnf_instance (:obj:`Cnf`)

    Return:
       A frozenset of all lits that appear in a Cnf.
    """
    return frozenset.union(*cnf_instance)

neg(literal)

Negate a Lit.

This function is an involution.

Parameters:

Name	Type	Description	Default
literal		obj:Lit): a Lit formed from a nonzero integer or from a Bool.	required

Return

Return the Lit cast from the negative of literal. If literal is of type Bool, then return TRUE for FALSE, FALSE for TRUE.

Source code in normal_form/cnf.py

def neg(literal: Lit) -> Lit:
    """Negate a Lit.

    This function is an involution.

    Args:
       literal (:obj:`Lit`): a Lit formed from a nonzero integer or from a Bool.

    Return:
       Return the Lit cast from the negative of ``literal``. If ``literal`` is of type
          Bool, then return ``TRUE`` for ``FALSE``, ``FALSE`` for ``TRUE``.

    """
    match literal.value:
        case Bool.TRUE:
            return lit(Bool.FALSE)
        case Bool.FALSE:
            return lit(Bool.TRUE)
        case int():
            return lit(-literal.value)
        case _ as unreachable:  # pragma: nocover
            assert_never(unreachable)

tautologically_reduce_clause(clause_instance)

Reduce a Clause using various tautologies.

The order in which these reductions are performed is important. This function is idempotent.

Tautologies affecting Clauses

(⊤ ∨ c = ⊤) (⊥ = ⊥) (⊥ ∨ c = c) (c ∨ ¬c = ⊤), where x is a Clause, ⊤ represents TRUE, ⊥ represents FALSE, and ∨ is disjunction.

Parameters:

Name	Type	Description	Default
clause_instance		obj:set[Lit]): an abstract set (a set or a frozenset) of Lits.	required

Return

The Clause formed by performing all the above-mentioned tautological reductions.

Source code in normal_form/cnf.py

def tautologically_reduce_clause(clause_instance: Clause) -> Clause:
    r"""Reduce a Clause using various tautologies.

    The order in which these reductions are performed is important. This function is
    idempotent.

    Tautologies affecting Clauses:
       (⊤ ∨ c = ⊤)  (⊥ = ⊥)  (⊥ ∨ c = c)  (c ∨ ¬c = ⊤),
       where `x` is a Clause, `⊤` represents ``TRUE``, `⊥` represents ``FALSE``, and `∨` is
          disjunction.

    Args:
       clause_instance (:obj:`set[Lit]`): an abstract set (a set or a frozenset) of Lits.

    Return:
       The Clause formed by performing all the above-mentioned tautological reductions.
    """
    if lit(Bool.TRUE) in clause_instance:
        return TRUE_CLAUSE
    if set(clause_instance) == {lit(Bool.FALSE)}:
        return FALSE_CLAUSE
    if lit(Bool.FALSE) in clause_instance:
        clause_instance = clause(
            [literal for literal in clause_instance if literal != lit(Bool.FALSE)])
    if not set(map(neg, clause_instance)).isdisjoint(clause_instance):
        return TRUE_CLAUSE
    return clause(clause_instance)

tautologically_reduce_cnf(cnf_instance)

Reduce a Cnf using various tautologies.

The order in which these reductions are performed is important. This function is idempotent. This is a recursive function that is guaranteed to terminate.

Tautologies affecting Cnfs

(x ∧ ⊥ = ⊥) (⊤ = ⊤) (⊤ ∧ x = x), where x is a Cnf, ⊤ represents TRUE, ⊥ represents FALSE, and ∧ is conjunction.

There is also a special reduction for Cnfs

(x ∧ y = x IF x < y), where x is a Cnf, y is another Cnf, and x < y means that every clause of x is also present as a clause in y.

Parameters:

Name	Type	Description	Default
cnf_instance		obj:set[set[Lit]]): an abstract set (set or frozenset) of abstract sets	required

Return

The Cnf formed by first reducing all the clauses tautologically and then performing all the above-mentioned tautological reductions on the Cnf itself.

Source code in normal_form/cnf.py

def tautologically_reduce_cnf(cnf_instance: Cnf) -> Cnf:
    r"""Reduce a Cnf using various tautologies.

    The order in which these reductions are performed is important. This function is
    idempotent. This is a recursive function that is guaranteed to terminate.

    Tautologies affecting Cnfs:
       (x ∧ ⊥ = ⊥)  (⊤ = ⊤)  (⊤ ∧ x = x),
       where `x` is a Cnf, `⊤` represents ``TRUE``, `⊥` represents ``FALSE``, and `∧` is
       conjunction.
    There is also a special reduction for Cnfs:
       (x ∧ y = x  IF  x < y),
       where `x` is a Cnf, `y` is another Cnf, and `x < y` means that every clause of `x`
       is also present as a clause in `y`.

    Args:
       cnf_instance (:obj:`set[set[Lit]]`): an abstract set (set or frozenset) of abstract sets
       of Lits.

    Return:
       The Cnf formed by first reducing all the clauses tautologically and then performing all
       the above-mentioned tautological reductions on the Cnf itself.
    """
    clause_set_reduced: set[Clause]
    clause_set_reduced = set(map(tautologically_reduce_clause, cnf_instance))

    if FALSE_CLAUSE in clause_set_reduced:
        return FALSE_CNF
    if clause_set_reduced == set(TRUE_CNF):
        return TRUE_CNF
    if TRUE_CLAUSE in clause_set_reduced:
        return tautologically_reduce_cnf(cnf(clause_set_reduced - TRUE_CNF))

    # Special reduction. x
    for clause1, clause2 in it.permutations(clause_set_reduced, 2):
        if clause1 < clause2:
            return tautologically_reduce_cnf(cnf(clause_set_reduced - {clause2}))

    return cnf(clause_set_reduced)

variable(positive_int)

Constructor-function for Variable type.

By definition, a Variable is just a positive integer. This function is idempotent.

Parameters:

Name	Type	Description	Default
positive_int		obj:int):	required

Return

If input is indeed positive, then return positive_int after casting to Variable.

Raises:

Type	Description
ValueError	if positive_int <= 0.

Source code in normal_form/cnf.py

def variable(positive_int: int | Variable) -> Variable:
    """Constructor-function for Variable type.

    By definition, a `Variable` is just a positive integer.  This
    function is idempotent.

    Args:
       positive_int (:obj:`int`):

    Return:
       If input is indeed positive, then return ``positive_int``
       after casting to Variable.

    Raises:
       ValueError: if ``positive_int <= 0``.
    """
    if positive_int <= 0:
        raise ValueError("Variable must be a positive integer.")
    return Variable(positive_int)

---

Last update: September 11, 2022