boofun.core.representations.cnf_form

Conjunctive Normal Form (CNF) representation for Boolean functions.

CNF represents a Boolean function as a conjunction (AND) of disjunctions (OR) of literals (variables or their negations).

Example: f(x₁,x₂,x₃) = (x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ x₂ ∨ x₃)

Functions

cnf_to_dnf(cnf)	Convert CNF to DNF using distribution laws.
create_cnf_from_maxterms(maxterms, n_vars)	Create CNF from list of maxterm indices.
is_satisfiable(cnf)	Check if CNF formula is satisfiable (SAT problem).

Classes

CNFClause(positive_vars, negative_vars)	A single clause in CNF form.
CNFFormula(clauses, n_vars)	CNF formula as a list of clauses.
CNFRepresentation()	CNF representation for Boolean functions.

class boofun.core.representations.cnf_form.CNFClause(positive_vars: Set[int], negative_vars: Set[int])

A single clause in CNF form.

positive_vars

Set of variables that appear positively

Type:

Set[int]

negative_vars

Set of variables that appear negatively

Type:

Set[int]

positive_vars: Set[int]

negative_vars: Set[int]

evaluate(x: List[int] | ndarray) → bool

Evaluate this CNF clause.

Parameters:

x – Binary input vector

Returns:

Boolean result of this clause (OR of all literals)

get_variables() → Set[int]

Get all variables in this clause.

is_tautology() → bool

Check if clause is a tautology (always true).

to_string(var_names: List[str] | None = None) → str

Convert clause to string representation.

Parameters:

var_names – Optional variable names, defaults to x₀, x₁, …

Returns:

String representation of the clause

to_dict() → Dict[str, Any]

Export clause to dictionary.

classmethod from_dict(data: Dict[str, Any]) → CNFClause

Create clause from dictionary.

__init__(positive_vars: Set[int], negative_vars: Set[int]) → None

class boofun.core.representations.cnf_form.CNFFormula(clauses: List[CNFClause], n_vars: int)

CNF formula as a list of clauses.

clauses

List of CNF clauses

Type:

List[boofun.core.representations.cnf_form.CNFClause]

n_vars

Number of variables

Type:

int

clauses: List[CNFClause]

n_vars: int

evaluate(x: List[int] | ndarray) → bool

Evaluate CNF formula.

Parameters:

x – Binary input vector

Returns:

Boolean result (AND of all clauses)

add_clause(clause: CNFClause) → None

Add a clause to the CNF formula.

simplify() → CNFFormula

Simplify CNF by removing tautologies and redundant clauses.

Returns:

Simplified CNF formula

to_string(var_names: List[str] | None = None) → str

Convert CNF to string representation.

Parameters:

var_names – Optional variable names

Returns:

String representation of CNF

to_dict() → Dict[str, Any]

Export CNF to dictionary.

classmethod from_dict(data: Dict[str, Any]) → CNFFormula

Create CNF from dictionary.

__init__(clauses: List[CNFClause], n_vars: int) → None

class boofun.core.representations.cnf_form.CNFRepresentation

CNF representation for Boolean functions.

evaluate(inputs: ndarray, data: CNFFormula, space: Space, n_vars: int) → bool | ndarray

Evaluate CNF representation.

Parameters:

• inputs – Input values (integer indices or binary vectors)

• data – CNF formula

• space – Evaluation space

• n_vars – Number of variables

Returns:

Boolean result(s)

dump(data: CNFFormula, space=None, **kwargs) → Dict[str, Any]

Export CNF representation.

convert_from(source_repr: BooleanFunctionRepresentation, source_data: Any, space: Space, n_vars: int, **kwargs) → CNFFormula

Convert from another representation to CNF.

Uses truth table method to generate maxterms.

convert_to(target_repr: BooleanFunctionRepresentation, source_data: Any, space: Space, n_vars: int, **kwargs) → ndarray

Convert CNF to another representation.

create_empty(n_vars: int, **kwargs) → CNFFormula

Create empty CNF (constant True).

is_complete(data: CNFFormula) → bool

Check if CNF is complete.

time_complexity_rank(n_vars: int) → Dict[str, int]

Return time complexity for CNF operations.

get_storage_requirements(n_vars: int) → Dict[str, int]

Return storage requirements for CNF representation.

boofun.core.representations.cnf_form.create_cnf_from_maxterms(maxterms: List[int], n_vars: int) → CNFFormula

Create CNF from list of maxterm indices.

Parameters:

• maxterms – List of maxterm indices where function is False

• n_vars – Number of variables

Returns:

CNF formula

boofun.core.representations.cnf_form.is_satisfiable(cnf: CNFFormula) → bool

Check if CNF formula is satisfiable (SAT problem).

This is a simplified check - full SAT solving is NP-complete.