sweetpea.core.cnf module

This module provides the core data types used in SweetPea Core.

Fundamentally, SweetPea deals with Boolean logic formulas written in conjunctive normal form (CNF). Wikipedia says:

a formula is in conjunctive normal form (CNF) […] if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs.

In SweetPea, we refer to the “literals” as Vars. These are combined into Clauses, which are then combined into CNFs. Most SweetPea functionality revolves around building and manipulating CNFs.

class sweetpea.core.cnf.Var(value)

Bases: object

A variable for use in a CNF formula.

This is essentially a wrapper for the builtin int type, but with a few advantages:

  • It is semantically distinct from an int, so reading code is more sensible.

  • Type aliases for int can be obnoxious to deal with because you may want to use int-supported operations (like addition, negation, etc), but these are not cross-type compatible (e.g., Var(3) + 2 produces an error in mypy).

  • We can implement custom behavior as a sort of micro-DSL without much overhead or issue.

Parameters

value (int) –

property value: int

The integer value of this variable.

class sweetpea.core.cnf.Clause(first_value=None, *rest_values)

Bases: sweetpea.core.simple_sequence.SimpleSequence[sweetpea.core.cnf.Var]

A sequence of Vars. A Clause indicates a logical disjunction between the contained variables. For example, Clause(Var(3), Var(7)) encodes (3 ∨ 7).

A Clause can also be instantiated with a list of Vars. This mode of instantiation will also accept raw ints in addition to instances of Var. For example, Clause([1, -2, 3]) corresponds to the formula (1 ∨ ¬2 ∨ 3).

class sweetpea.core.cnf.CNF(*values)

Bases: sweetpea.core.simple_sequence.SimpleSequence[sweetpea.core.cnf.Clause]

A conjunction of disjunction Clauses. For example, CNF(Clause(Var(3), Var(7)), Clause(Var(1), Var(13))) corresponds to the CNF formula ((3 ∨ 7) ∧ (1 ∨ 13)).

CNFs can also be instantiated with a list of lists of Vars, where each inner list represents a Clause and the outer list represents the CNF formula itself. Similar to Clause, this mode of instantiation will also accept raw ints in addition to instances of Var. For example, CNF([[1, 2, -3], [-2, 7, 1]]) corresponds to the CNF formula ((1 ∨ 2 ∨ ¬3) ∧ (¬2 ∨ 7 ∨ 1)).

static from_fresh(fresh)

Returns an empty CNF with the given number of fresh Vars already allocated.

Note

This method probably shouldn’t exist! The number of fresh variables should be deduced from the formulas themselves. This exists for legacy compatibility and should eventually be removed.

Parameters

fresh (int) –

Return type

sweetpea.core.cnf.CNF

static and_vars(a, b)

Returns a CNF formula encoding (a ∧ b).

Parameters
Return type

sweetpea.core.cnf.CNF

static or_vars(a, b)

Returns a CNF formula encoding (a ∨ b).

Parameters
Return type

sweetpea.core.cnf.CNF

static xor_vars(a, b)

Returns a CNF formula encoding (a ⊕ b) as ((a ∨ b) ∧ (¬a ∨ ¬b)).

Parameters
Return type

sweetpea.core.cnf.CNF

static xnor_vars(a, b)

Returns a CNF formula encoding (a ⊙ b) as ((a ∨ ¬b) ∧ (¬a ∨ b)).

Note

(a ⊙ b) is logically equivalent to (a ⇔ b), so this function replaces the original Haskell version’s doubleImplies function.

Parameters
Return type

sweetpea.core.cnf.CNF

static distribute(v, cnf)

Distributes the given Var across each Clause of the given CNF formula, producing a new :class`CNF`.

Parameters
Return type

sweetpea.core.cnf.CNF

as_dimacs_string(fresh_variable_count=None)

Represents the CNF as a string in the DIMACS format.

The DIMACS format is a standardized method of representing CNF formulas as strings. This implementation is based on the details given here.

Parameters

fresh_variable_count (Optional[int]) –

Return type

str

as_unigen_string(fresh_variable_count=None, support_set_length=None, sampled_variables=None)

Returns a string representing the CNF formula in the modified DIMACS format used by Unigen.

See CNF.as_dimacs_string() for details about the DIMACS format.

Unigen adds an extra line at the top that describes the list of variables you would like to sample (instead of sampling among all variables). This line is given in the form:

c ind v1 v2 ... vn 0

where v1, v2, …, vn represent variables in the formula. This line is placed just below the “problem” line (the line beginning with p).

Parameters

  • fresh_variable_count (Optional[int]) –

  • support_set_length (Optional[int]) –

  • sampled_variables (Optional[List[sweetpea.core.cnf.Var]]) –

Return type

str

as_list_of_list_of_ints()

Converts the CNF to a list of lists of ints.

Return type

List[List[int]]

as_haskell_cnf()

Converts the CNF to a tuple whose first element is the number of fresh variables in the formula and whose second element is the CNF represented as a list of lists of ints.

Note

This is the way CNF formulas were encoded in the original Haskell code. It only exists for consistency checks across the two code bases.

Return type

Tuple[int, List[List[int]]]

get_fresh()

Creates a new Var for the formula.

Return type

sweetpea.core.cnf.Var

get_n_fresh(n)

Creates the next n Vars, numbered sequentially.

Parameters

n (int) –

Return type

List[sweetpea.core.cnf.Var]

append(other)

Appends a CNF to this CNF.

Parameters

other (Union[sweetpea.core.cnf.CNF, sweetpea.core.cnf.Clause, Iterable[sweetpea.core.cnf.Clause], sweetpea.core.cnf.Var]) –

prepend(other)

Prepends a CNF to this CNF.

Parameters

other (Union[sweetpea.core.cnf.CNF, sweetpea.core.cnf.Clause, Iterable[sweetpea.core.cnf.Clause], sweetpea.core.cnf.Var]) –

set_to_zero(variable)

Zeroes the specified Var by appending its negation to the existing CNF formula.

Parameters

variable (sweetpea.core.cnf.Var) –

zero_out(in_list)

Appends a CNF formula negating the existing CNF formula.

Parameters

in_list (Iterable[sweetpea.core.cnf.Var]) –

set_to_one(variable)

Sets the specified variable to 1 by appending it to the existing CNF formula.

Parameters

variable (sweetpea.core.cnf.Var) –

assert_k_of_n(k, in_list)
Parameters
assert_k_less_than_n(k, in_list)
Parameters
assert_k_greater_than_n(k, in_list)
Parameters
pop_count(in_list)

Returns the list of Vars that represents the bits of the given list variable in binary.

Parameters

in_list (Sequence[sweetpea.core.cnf.Var]) –

Return type

List[sweetpea.core.cnf.Var]

half_adder(a, b)
Parameters
Return type

Tuple[sweetpea.core.cnf.Var, sweetpea.core.cnf.Var]

full_adder(a, b, cin)
Parameters
Return type

Tuple[sweetpea.core.cnf.Var, sweetpea.core.cnf.Var]

ripple_carry(xs, ys)
Parameters
Return type

Tuple[List[sweetpea.core.cnf.Var], List[sweetpea.core.cnf.Var]]