sweetpea.logic module

This module provides functionality for handling logic formulas.

class sweetpea.logic.And(input_list)

Bases: tuple

Create new instance of And(input_list,)

property input_list

Alias for field number 0

class sweetpea.logic.Or(input_list)

Bases: tuple

Create new instance of Or(input_list,)

property input_list

Alias for field number 0

class sweetpea.logic.If(p, q)

Bases: tuple

Create new instance of If(p, q)

property p

Alias for field number 0

property q

Alias for field number 1

class sweetpea.logic.Iff(p, q)

Bases: tuple

Create new instance of Iff(p, q)

property p

Alias for field number 0

property q

Alias for field number 1

class sweetpea.logic.Not(c)

Bases: tuple

Create new instance of Not(c,)

property c

Alias for field number 0

sweetpea.logic.to_cnf_naive(f, next_variable)

Converts to CNF using the pattern described on https://en.wikipedia.org/wiki/Conjunctive_normal_form#Converting_from_first-order_logic.

The conversion is naive, which means it is subject to an exponential explosion in the length of the formula. The upside is that it does not introduce any new variables, which constrains the overall size of the solution space. (#SAT)

Parameters
Return type

Tuple[sweetpea.logic.And, int]

sweetpea.logic.to_cnf_switching(f, next_variable)

Converts to CNF using the pattern described on https://en.wikipedia.org/wiki/Conjunctive_normal_form#Converting_from_first-order_logic.

However, distributing ORs over ANDs is done via switching variables, to keep the converted formula small, as described here at https://www.cs.jhu.edu/~jason/tutorials/convert-to-CNF.html.

Parameters
Return type

Tuple[sweetpea.logic.And, int]

sweetpea.logic.to_cnf_tseitin(f, next_variable)

Converts to CNF using the Tseitin transformation. This will introduce addtional variables, which will increase #SAT, but provides a linear bound on the length increase of the new formula. See https://en.wikipedia.org/wiki/Tseytin_transformation.

Parameters
Return type

Tuple[sweetpea.logic.And, int]

sweetpea.logic.cnf_to_json(formula)
Parameters

formula (List[sweetpea.logic.And]) –

Return type

List[List[int]]