cnfformula package

Module contents

class CNF(clauses=None, header=None)

Bases: object

Propositional formulas in conjunctive normal form.

A CNF formula is a sequence of clauses, which are sequences of literals. Each literal is either a variable or its negation.

Use add_variable method to add a variable to the formula. Two variable with the same name are considered the same variable, add successive additions do not have any effect.

Use add_clause to add new clauses to CNF. Clauses will be added multiple times in case of multiple insertion of the same clauses.

For documentation purpose it is possible use have an additional comment header at the top of the formula, which will be optionally exported to LaTeX or dimacs.

Implementation: for efficiency reason clauses and variable can only be added, and not deleted. Furthermore order matters in the representation.

Examples

>>> c=CNF([ [(True,"x1"),(True,"x2"),(False,"x3")],               [(False,"x2"),(True,"x4")] ])
>>> print( c.dimacs(export_header=False) )
p cnf 4 2
1 2 -3 0
-2 4 0
>>> c.add_clause( [(False,"x3"),(True,"x4"),(False,"x5")] )
>>> print( c.dimacs(export_header=False))
p cnf 5 3
1 2 -3 0
-2 4 0
-3 4 -5 0
Attributes:
header

Header getter

Methods

add_clause(clause[, literal_repetitions, …]) Add a clause to the CNF.
add_clause_unsafe(clause) Add a clause without checking input
add_variable(var[, description]) Add a variable to the formula (if not already resent).
binary_mapping(D, R, **kwargs) Binary CNF representation of a mapping between two sets.
clauses() Return the list of clauses
dimacs([export_header, extra_text]) Produce the dimacs encoding of the formula
equal_to_constraint(variables, value) Clauses encoding a “equal to” constraint
exactly_half_ceil(variables) Clauses encoding a “exactly half” constraint (rounded up)
exactly_half_floor(variables) Clauses encoding a “exactly half” constraint (rounded down)
greater_or_equal_constraint(variables, …) Clauses encoding a “greater than or equal to” constraint
greater_than_constraint(variables, lowerbound) Clauses encoding a “strictly greater than” constraint
is_satisfiable([cmd, sameas, verbose]) Determines whether a CNF is satisfiable or not.
latex([export_header, extra_text, full_document]) Output a LaTeX version of the CNF formula
less_or_equal_constraint(variables, upperbound) Clauses encoding a “less than or equal to” constraint
less_than_constraint(variables, upperbound) Clauses encoding a “strictly less than” constraint
loose_majority_constraint(variables) Clauses encoding a “at least half” constraint
loose_minority_constraint(variables) Clauses encoding a “at most half” constraint
parity_constraint(variables, constant) Output the CNF encoding of a parity constraint
unary_mapping(D, R, **kwargs) Unary CNF representation of a mapping between two sets.
variables() Returns (a copy of) the list of variable names.
add_clause(clause, literal_repetitions=False, opposite_literals=False, auto_variables=True, strict=False)

Add a clause to the CNF.

E.g. (not x3) or x4 or (not x2) is encoded as
[(False,u”x3”),(True,u”x4”),(False,u”x2”)]

All variable mentioned in the clause will be added to the list of variables of the CNF, in the order of appearance in the clauses, unless auto_variable is False.

Parameters:
clause: list of (bool,str)

the clause to be added in the CNF

A clause with k literals is a list with k pairs. First coords are the polarities, second coords are utf8 encoded strings with variable names.

Clause may contain repeated or opposite literal, but this behavior can be modified by the optional flags.

Clauses are added with repetition, i.e. if the same clause is added twice then it will occur twice in the formula too.

literal_repetitions: bool, optional

True if and only if the clause can have repeated literal.

Useful for sanity check. If the flag is False and the clause contain two copies of the same literal, then ValueError is raised. (default: False)

opposite_literals: bool, optional

True if and only if the clause can have opposite literal.

Useful for sanity check. If the flag is False and the clause contain two opposite literals, then ValueError is raised. (default: False)

auto_variables: bool, optional

If True the clause can contain new variables.

New variables occurring in the clause will be added to the formula, unless the flag is False. In that case when a clause contains an unknow variables, ValueError is raised. (default: True)

strict: bool, optional

If True impose restrictions on the clause.

Setting this to True is equivalent to set literal_repetitions, opposite_literals, auto_variables to False. In case of conflicting settings, the most restrictive one holds. (default: False)
add_clause_unsafe(clause)

Add a clause without checking input

This is logically equivalent to CNF.add_clause() where literal_repetition, opposite_literals and auto_variables are True, but it is faster because it does less checks on the input.

Parameters:
clause: list of (bool,str)

the clause to be added in the CNF

A clause with k literals is a list with k pairs. First coords are the polarities, second coords are utf8 encoded strings with variable names.

Clauses are added with repetition, i.e. if the same clause is added twice then it will occur twice in the formula too.
Raises:
KeyError

if the clause contains a variable which was not added to the formula before.
add_variable(var, description=None)

Add a variable to the formula (if not already resent).

The variable must be hashable. I.e. it must be usable as key in a dictionary. It raises TypeError if the variable cannot be hashed.

Parameters:
var: hashable

the variable name to be added/updated. It can be any hashable object (i.e. a dictionary key).

description: str, optional

an explanation/description/comment about the variable.
class binary_mapping(D, R, **kwargs)

Bases: object

Binary CNF representation of a mapping between two sets.

Attributes:
Bits
Domain
Range

Methods

forbid_bitstring(i, bs) Generates a clause that exclude ‘i -> bs’ mapping
forbid_image(i, j) Generates a clause that exclude ‘i -> j’ mapping
bitstring_to_image  
clauses  
image_to_bitstring  
var_name  
variables  
Bits = None
Domain = None
Injective = False
NonDecreasing = False
Range = None
bitstring_to_image(bs)
clauses()
forbid_bitstring(i, bs)

Generates a clause that exclude ‘i -> bs’ mapping

forbid_image(i, j)

Generates a clause that exclude ‘i -> j’ mapping

image_to_bitstring(im)
static var_name(i, b)
variables()
clauses()

Return the list of clauses

dimacs(export_header=True, extra_text=None)

Produce the dimacs encoding of the formula

The formula is rendered in the DIMACS format for CNF formulas, which is a particularly popular input format for SAT solvers [1].

Parameters:
export_header : bool

determines whether the formula header should be inserted as a comment in the DIMACS output.

extra_text : str, optional

Additional text attached to the header
Returns:
string

the string contains the Dimacs code

References

[1](1, 2) http://www.satlib.org/Benchmarks/SAT/satformat.ps

Examples

>>> c=CNF([[(False,"x_1"),(True,"x_2"),(False,"x_3")],                   [(False,"x_2"),(False,"x_4")],                    [(True,"x_2"),(True,"x_3"),(False,"x_4")]])
>>> print(c.dimacs(export_header=False))
p cnf 4 3
-1 2 -3 0
-2 -4 0
2 3 -4 0

>>> c=CNF()
>>> print(c.dimacs(export_header=False))
p cnf 0 0
classmethod equal_to_constraint(variables, value)

Clauses encoding a “equal to” constraint

E.g. X1 + X2 + X3 + X4 = 1

(X1 v X2 v X3 v X4) (~X1 v ~X2) (~X1 v ~X3) (~X1 v ~X4) (~X2 v ~X3) (~X2 v ~X4) (~X3 v ~X4)

Parameters:
variables : list of variables

variables in the constraint

value: int

target values
Returns:
a list of clauses
classmethod exactly_half_ceil(variables)

Clauses encoding a “exactly half” constraint (rounded up)

Parameters:
variables : list of variables

variables in the constraint
Returns:
a list of clauses
classmethod exactly_half_floor(variables)

Clauses encoding a “exactly half” constraint (rounded down)

Parameters:
variables : list of variables

variables in the constraint
Returns:
a list of clauses
classmethod greater_or_equal_constraint(variables, lowerbound)

Clauses encoding a “greater than or equal to” constraint

E.g. X1 + X2 + X3 + X4 > 1

(X1 v X2 v X3) (X1 v X2 v X4) (X1 v X3 v X4) (X2 v X3 v X4)

Parameters:
variables : list of variables

variables in the constraint

lowerbound: int

lower bound of the constraint
Returns:
a list of clauses

Examples

>>> tuple(CNF.greater_than_constraint(['a','b','c'],1)) == tuple(CNF.greater_or_equal_constraint(['a','b','c'],2))
True
>>> list(CNF.greater_or_equal_constraint(['a','b','c'],3))
[[(True, 'a')], [(True, 'b')], [(True, 'c')]]
>>> list(CNF.greater_or_equal_constraint(['a'],0))
[]
>>> list(CNF.greater_or_equal_constraint(['a','b','c'],4))
[[]]
classmethod greater_than_constraint(variables, lowerbound)

Clauses encoding a “strictly greater than” constraint

E.g. X1 + X2 + X3 + X4 > 2

(X1 v X2 v X3) (X1 v X2 v X4) (X1 v X3 v X4) (X2 v X3 v X4)

Parameters:
variables : list of variables

variables in the constraint

lowerbound: int

lower bound of the constraint
Returns:
a list of clauses

Examples

>>> list(CNF.greater_than_constraint(['a','b','c'],2))
[[(True, 'a')], [(True, 'b')], [(True, 'c')]]
>>> list(CNF.greater_than_constraint(['a'],0))
[[(True, 'a')]]
>>> list(CNF.greater_than_constraint(['a','b','c'],-1))
[]
>>> list(CNF.greater_than_constraint(['a','b','c'],3))
[[]]
header

Header getter

is_satisfiable(cmd=None, sameas=None, verbose=0)

Determines whether a CNF is satisfiable or not.

The formula is passed to a SAT solver, according to the optional command line cmd. If no command line is specified, the known solvers are tried in succession until one is found.

It is possible to use any drop-in replacement for these solvers, but in this case more information is needed on how to communicate with the solver. In particular minisat does not respect the standard DIMACS I/O conventions, and that holds also for glucose which is a drop-in replacement of minisat.

For the supported solver we can pick the right interface, but for other solvers it is impossible to guess. Nevertheless it is possible to indicate which interface to use, or more specifically which known solver interface to mimic.

>>> F.is_satisfiable(cmd='minisat-style-solver',sameas='minisat')  
>>> F.is_satisfiable(cmd='dimacs-style-solver',sameas='lingeling')
Parameters:
cmd : string,optional

the actual command line used to invoke the SAT solver

sameas : string, optional

use the interface of one of the supported solvers. Useful when the solver used in the command line is not supported.

verbose: int

0 or less means no output. 1 shows the command line actually run. 2 outputs the solver output. (default: 0)
Returns:
(boolean,assignment or None)

A pair (answer,witness) where answer is either True when F is satisfiable, or False otherwise. If F is satisfiable the witness is a satisfiable assignment in form of a dictionary, otherwise it is None.
Raises:
RuntimeError

if it is not possible to correctly invoke the solver needed.

ValueError

if sameas is set and is not the name of a supported solver.

TypeError

if F is not a CNF object.

See also

cnfformula.utils.solver.is_satisfiable
implementation independent of CNF object.
cnfformula.utils.solver.supported_satsolvers
the SAT solver recognized by cnfformula.

Examples

>>> F.is_satisfiable()                                              
>>> F.is_satisfiable(cmd='minisat -no-pre')                         
>>> F.is_satisfiable(cmd='glucose -pre')                            
>>> F.is_satisfiable(cmd='lingeling --plain')                       
>>> F.is_satisfiable(cmd='sat4j')                                   
>>> F.is_satisfiable(cmd='my-hacked-minisat -pre',sameas='minisat') 
>>> F.is_satisfiable(cmd='patched-lingeling',sameas='lingeling')
latex(export_header=True, extra_text=None, full_document=False)

Output a LaTeX version of the CNF formula

The CNF formula is translated into the LaTeX markup language [1], using the names of the variable literally. The formula is rendered in the align environment, with one clause per row. Negated literals are rendered using the \neg command.

The output string is ready to be included in a document, but it does not include neither a preamble nor is nested inside \begin{document} … \end{document}.

Parameters:
export_header : bool, optional

determines whether the formula header should be inserted as a LaTeX comment in the output. By default is True.

extra_text : str, optional

Additional text attached to the abstract.

full_document : bool, optional

rather than just output the formula, output a document that contains it. False by default.
Returns:
string

the string contains the LaTeX code

References

[1](1, 2) http://www.latex-project.org/

Examples

>>> c=CNF([[(False,"x_1"),(True,"x_2"),(False,"x_3")],                   [(False,"x_2"),(False,"x_4")],                    [(True,"x_2"),(True,"x_3"),(False,"x_4")]])
>>> print(c.latex(export_header=False))
\begin{align}
&       \left( {\overline{x}_1} \lor            {x_2} \lor {\overline{x}_3} \right) \\
& \land \left( {\overline{x}_2} \lor {\overline{x}_4} \right) \\
& \land \left(            {x_2} \lor            {x_3} \lor {\overline{x}_4} \right)
\end{align}
>>> c=CNF()
>>> print(c.latex(export_header=False))
\begin{align}
   \top
\end{align}
classmethod less_or_equal_constraint(variables, upperbound)

Clauses encoding a “less than or equal to” constraint

E.g. X1 + X2 + X3 + X4 <= 2

(~X1 v ~X2 v ~X3) (~X1 v ~X2 v ~X4) (~X1 v ~X3 v ~X4) (~X2 v ~X3 v ~X4)

Parameters:
variables : list of variables

variables in the constraint

upperbound: int

upper bound of the constraint
Returns:
a list of clauses

Examples

>>> list(CNF.less_than_constraint(['a','b','c'],3)) == list(CNF.less_or_equal_constraint(['a','b','c'],2))
True
>>> list(CNF.less_or_equal_constraint(['a','b','c'],1))
[[(False, 'a'), (False, 'b')], [(False, 'a'), (False, 'c')], [(False, 'b'), (False, 'c')]]
>>> list(CNF.less_or_equal_constraint(['a','b'],0))
[[(False, 'a')], [(False, 'b')]]
>>> list(CNF.less_or_equal_constraint(['a','b','c'],-1))
[[]]
>>> list(CNF.less_or_equal_constraint(['a','b','c'],10))
[]
classmethod less_than_constraint(variables, upperbound)

Clauses encoding a “strictly less than” constraint

E.g. X1 + X2 + X3 + X4 < 3

(~X1 v ~X2 v ~X3) (~X1 v ~X2 v ~X4) (~X1 v ~X3 v ~X4) (~X2 v ~X3 v ~X4)

Parameters:
variables : list of variables

variables in the constraint

upperbound: int

upper bound of the constraint
Returns:
a list of clauses

Examples

>>> list(CNF.less_than_constraint(['a','b','c'],2))
[[(False, 'a'), (False, 'b')], [(False, 'a'), (False, 'c')], [(False, 'b'), (False, 'c')]]
>>> list(CNF.less_than_constraint(['a'],1))
[[(False, 'a')]]
>>> list(CNF.less_than_constraint(['a','b','c'],-1))
[[]]
>>> list(CNF.less_than_constraint(['a','b','c'],10))
[]
classmethod loose_majority_constraint(variables)

Clauses encoding a “at least half” constraint

Parameters:
variables : list of variables

variables in the constraint
Returns:
a list of clauses
classmethod loose_minority_constraint(variables)

Clauses encoding a “at most half” constraint

Parameters:
variables : list of variables

variables in the constraint
Returns:
a list of clauses
classmethod parity_constraint(variables, constant)

Output the CNF encoding of a parity constraint

E.g. X1 + X2 + X3 = 1 (mod 2) is encoded as

( X1 v X2 v X3) (~X1 v ~X2 v X3) (~X1 v X2 v ~X3) ( X1 v ~X2 v ~X3)

Parameters:
variables : array-like

variables involved in the constraint

constant : {0,1}

the constant of the linear equation
Returns:
a list of clauses

Examples

>>> list(CNF.parity_constraint(['a','b'],1))
[[(True, 'a'), (True, 'b')], [(False, 'a'), (False, 'b')]]
>>> list(CNF.parity_constraint(['a','b'],0))
[[(True, 'a'), (False, 'b')], [(False, 'a'), (True, 'b')]]
>>> list(CNF.parity_constraint(['a'],0))
[[(False, 'a')]]
class unary_mapping(D, R, **kwargs)

Bases: object

Unary CNF representation of a mapping between two sets.

Attributes:
Domain
Pattern
Range

Methods

clauses  
counterimages  
domain  
images  
range  
var_name  
variables  
Complete = False
Domain = None
Functional = False
Injective = False
NonDecreasing = False
Pattern = None
Range = None
Surjective = False
clauses()
counterimages(r)
domain()
images(d)
range()
static var_name(i, b)
variables()
variables()

Returns (a copy of) the list of variable names.

readGraph(input_file, graph_type, file_format='autodetect', multi_edges=False)

Read a Graph from file

The graph are managed using the NetworkX library, and most of the input and output formats are the ones supported by it. Plus we added support for some more hackish formats that are useful in applications.

for the “simple” and “bipartite” types, the graph is actually a (Multi)Graph object, while it is a (Multi)DiGraph in case of “dag” or “digraph”.

In the case of “dag” type, the graph is guaranteed to be acyclic and to pass the is_dag test. In the case of “bipartite” type, the graph is guaranteed to have the two parts labeled and to pass the has_bipartition test.

Parameters:
input_file: str, unicode or file-like object

the input file from which the graph is read. If it is a string then the graph is read from a file with that string as filename. Otherwise if the input_file is a file object (or a text stream), the graph is read from there.

graph_type: string in {“simple”,”digraph”,”dag”,”bipartite”}

see also cnfformula.graph.supported_formats()

file_format: string, optional

The file format that the parser should expect to receive. See also cnfformula.graph.supported_formats(). By default it tries to autodetect it from the file name extension (when applicable).

multi_edges: bool,optional

are multiple edge allowed in the graph? By default this is not allowed.
Returns:
a graph object

one among networkx.DiGraph, networkx.MultiDiGraph, networkx.Graph, networkx.MultiGraph object.
Raises:
ValueError

raised when either input_file is neither a file object nor a string, or when graph_type and file_format are invalid choices.

IOError

it is impossible to read the input_file

See also

writeGraph, is_dag, has_bipartition

writeGraph(G, output_file, graph_type, file_format='autodetect')

Write a graph to a file

Parameters:
G : networkx.Graph (or similar)
output_file: file object

the output file to which the graph is written. If it is a string then the graph is written to a file with that string as filename. Otherwise if output_file is a file object (or a text stream), the graph is written there.

graph_type: string in {“simple”,”digraph”,”dag”,”bipartite”}

see also cnfformula.graph.supported_formats()

file_format: string, optional

The file format that the parser should expect to receive. See also cnfformula.graph.supported_formats(). By default it tries to autodetect it from the file name extension (when applicable).
Returns:
None
Raises:
ValueError

raised when either output_file is neither a file object nor a string, or when graph_type and file_format are invalid choices.

IOError

it is impossible to write on the output_file

See also

readGraph

RamseyLowerBoundFormula(s, k, N)

Formula claiming that Ramsey number r(s,k) > N

Arguments: - s: independent set size - k: clique size - N: vertices

PebblingFormula(digraph)

Pebbling formula

Build a pebbling formula from the directed graph. If the graph has an ordered_vertices attribute, then it is used to enumerate the vertices (and the corresponding variables).

Arguments: - digraph: directed acyclic graph.

GraphColoringFormula(G, colors, functional=True)

Generates the clauses for colorability formula

The formula encodes the fact that the graph \(G\) has a coloring with color set colors. This means that it is possible to assign one among the elements in ``colors``to that each vertex of the graph such that no two adjacent vertices get the same color.

Parameters:
G : networkx.Graph

a simple undirected graph

colors : list or positive int

a list of colors or a number of colors
Returns:
CNF

the CNF encoding of the coloring problem on graph G
GraphOrderingPrinciple(graph, total=False, smart=False, plant=False, knuth=0)

Generates the clauses for graph ordering principle

Arguments: - graph : undirected graph - total : add totality axioms (i.e. “x < y” or “x > y”) - smart : “x < y” and “x > y” are represented by a single variable (implies total) - plant : allow last element to be minimum (and could make the formula SAT) - knuth : Don Knuth variants 2 or 3 of the formula (anything else suppress it)

SubsetCardinalityFormula(B, equalities=False)

Consider a bipartite graph \(B\). The CNF claims that at least half of the edges incident to each of the vertices on left side of \(B\) must be zero, while at least half of the edges incident to each vertex on the left side must be one.

Variants of these formula on specific families of bipartite graphs have been studied in [1], [2] and [3], and turned out to be difficult for resolution based SAT-solvers.

Each variable of the formula is denoted as \(x_{i,j}\) where \(\{i,j\}\) is an edge of the bipartite graph. The clauses of the CNF encode the following constraints on the edge variables.

For every left vertex i with neighborhood \(\Gamma(i)\)

\[\sum_{j \in \Gamma(i)} x_{i,j} \geq \frac{|\Gamma(i)|}{2}\]

For every right vertex j with neighborhood \(\Gamma(j)\)

\[\sum_{i \in \Gamma(j)} x_{i,j} \leq \frac{|\Gamma(j)|}{2}.\]

If the equalities flag is true, the constraints are instead represented by equations.

\[\sum_{j \in \Gamma(i)} x_{i,j} = \left\lceil \frac{|\Gamma(i)|}{2} \right\rceil\]
\[\sum_{i \in \Gamma(j)} x_{i,j} = \left\lfloor \frac{|\Gamma(j)|}{2} \right\rfloor .\]
Parameters:
B : networkx.Graph

the graph vertices must have the ‘bipartite’ attribute set. Left vertices must have it set to 0 and the right ones to 1. A KeyException is raised otherwise.

equalities : boolean

use equations instead of inequalities to express the cardinality constraints. (default: False)
Returns:
A CNF object

References

[1](1, 2) Mladen Miksa and Jakob Nordstrom Long proofs of (seemingly) simple formulas Theory and Applications of Satisfiability Testing–SAT 2014 (2014)
[2](1, 2) Ivor Spence sgen1: A generator of small but difficult satisfiability benchmarks Journal of Experimental Algorithmics (2010)
[3](1, 2) Allen Van Gelder and Ivor Spence Zero-One Designs Produce Small Hard SAT Instances Theory and Applications of Satisfiability Testing–SAT 2010(2010)
PigeonholePrinciple(pigeons, holes, functional=False, onto=False)

Pigeonhole Principle CNF formula

The pigeonhole principle claims that no M pigeons can sit in N pigeonholes without collision if M>N. The counterpositive CNF formulation requires such mapping to be satisfied. There are different variants of this formula, depending on the values of functional and onto argument.

  • PHP: pigeon can sit in multiple holes
  • FPHP: each pigeon sits in exactly one hole
  • onto-PHP: pigeon can sit in multiple holes, every hole must be
    covered.
  • Matching: one-to-one bijection between pigeons and holes.

Arguments: - pigeon: number of pigeons - hole: number of holes - functional: add clauses to enforce at most one hole per pigeon - onto: add clauses to enforce that any hole must have a pigeon

>>> print(PigeonholePrinciple(4,3).dimacs(export_header=False))
p cnf 12 22
1 2 3 0
4 5 6 0
7 8 9 0
10 11 12 0
-1 -4 0
-1 -7 0
-1 -10 0
-4 -7 0
-4 -10 0
-7 -10 0
-2 -5 0
-2 -8 0
-2 -11 0
-5 -8 0
-5 -11 0
-8 -11 0
-3 -6 0
-3 -9 0
-3 -12 0
-6 -9 0
-6 -12 0
-9 -12 0
CliqueFormula(G, k)

Test whether a graph has a k-clique.

Given a graph \(G\) and a non negative value \(k\), the CNF formula claims that \(G\) contains a \(k\)-clique.

Parameters:
G : networkx.Graph

a simple graph

k : a non negative integer

clique size
Returns:
a CNF object
BinaryPigeonholePrinciple(pigeons, holes)

Binary Pigeonhole Principle CNF formula

The pigeonhole principle claims that no M pigeons can sit in N pigeonholes without collision if M>N. This formula encodes the principle using binary strings to identify the holes.

Parameters:
pigeon : int

number of pigeons

holes : int

number of holes
SubgraphFormula(graph, templates, symmetric=False)

Test whether a graph contains one of the templates.

Given a graph \(G\) and a sequence of template graphs \(H_1\), \(H_2\), …, \(H_t\), the CNF formula claims that \(G\) contains an isomorphic copy of at least one of the template graphs.

E.g. when \(H_1\) is the complete graph of \(k\) vertices and it is the only template, the formula claims that \(G\) contains a \(k\)-clique.

Parameters:
graph : networkx.Graph

a simple graph

templates : list-like object

a sequence of graphs.

symmetric:

all template graphs are symmetric wrt permutations of vertices. This allows some optimization in the search space of the assignments.

induce:

force the subgraph to be induced (i.e. no additional edges are allowed)
Returns:
a CNF object
GraphIsomorphism(G1, G2)

Graph Isomorphism formula

The formula is the CNF encoding of the statement that two simple graphs G1 and G2 are isomorphic.

Parameters:
G1 : networkx.Graph

an undirected graph object

G2 : networkx.Graph

an undirected graph object
Returns:
A CNF formula which is satiafiable if and only if graphs G1 and G2
are isomorphic.
OrderingPrinciple(size, total=False, smart=False, plant=False, knuth=0)

Generates the clauses for ordering principle

Arguments: - size : size of the domain - total : add totality axioms (i.e. “x < y” or “x > y”) - smart : “x < y” and “x > y” are represented by a single variable (implies totality) - plant : allow a single element to be minimum (could make the formula SAT) - knuth : Donald Knuth variant of the formula ver. 2 or 3 (anything else suppress it)

PythagoreanTriples(N)

There is a Pythagorean triples free coloring on N

The formula claims that it is possible to bicolor the numbers from 1 to \(N\) so that there is no monochromatic triplet \((x,y,z)\) so that \(x^2+y^2=z^2\).

Parameters:
N : int

size of the interval
Raises:
ValueError

Parameters are not positive integers

References

[1]M. J. Heule, O. Kullmann, and V. W. Marek. Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. arXiv preprint arXiv:1605.00723, 2016.
StoneFormula(D, nstones)

Stone formulas

The stone formulas have been introduced in [2] and generalized in [1]. They are one of the classic examples that separate regular resolutions from general resolution [1].

A “Stones formula” from a directed acyclic graph \(D\) claims that each vertex of the graph is associated with one on \(s\) stones (not necessarily in an injective way). In particular for each vertex \(v\) in \(V(D)\) and each stone \(j\) we have a variable \(P_{v,j}\) that claims that stone \(j\) is associated to vertex \(v\).

Each stone can be either red or blue, and not both. The propositional variable \(R_j\) if true when the stone \(j\) is red and false otherwise.

The clauses of the formula encode the following constraints. If a stone is on a source vertex (i.e. a vertex with no incoming edges), then it must be red. If all stones on the predecessors of a vertex are red, then the stone of the vertex itself must be red.

The formula furthermore enforces that the stones on the sinks (i.e. vertices with no outgoing edges) are blue.

Note

The exact formula structure depends by the graph and on its topological order, which is determined by the enumerate_vertices(D).

Parameters:
D : a directed acyclic graph

it should be a directed acyclic graph.

nstones : int

the number of stones.
Raises:
ValueError

if \(D\) is not a directed acyclic graph

ValueError

if the number of stones is negative

References

[1](1, 2, 3) M. Alekhnovich, J. Johannsen, T. Pitassi and A. Urquhart An Exponential Separation between Regular and General Resolution. Theory of Computing (2007)
[2](1, 2) R. Raz and P. McKenzie Separation of the monotone NC hierarchy. Combinatorica (1999)
EvenColoringFormula(G)

Even coloring formula

The formula is defined on a graph \(G\) and claims that it is possible to split the edges of the graph in two parts, so that each vertex has an equal number of incident edges in each part.

The formula is defined on graphs where all vertices have even degree. The formula is satisfiable only on those graphs with an even number of vertices in each connected component [1].

Returns:
CNF object
Raises:
ValueError

if the graph in input has a vertex with odd degree

References

[1](1, 2) Locality and Hard SAT-instances, Klas Markstrom Journal on Satisfiability, Boolean Modeling and Computation 2 (2006) 221-228
RamseyWitnessFormula(G, k, s)

Test whether a graph contains one of the templates.

Given a graph \(G\) and a non negative values \(k\) and \(s\), the CNF formula claims that \(G\) contains a neither a \(k\)-clique nor an independet set of size \(s\).

Parameters:
G : networkx.Graph

a simple graph

k : a non negative integer

clique size

s : a non negative integer

independet set size
Returns:
a CNF object
DominatingSet(G, d, alternative=False)

Generates the clauses for a dominating set for G of size <= d

The formula encodes the fact that the graph \(G\) has a dominating set of size \(d\). This means that it is possible to pick at most \(d\) vertices in \(V(G)\) so that all remaining vertices have distance at most one from the selected ones.

Parameters:
G : networkx.Graph

a simple undirected graph

d : a positive int

the size limit for the dominating set

alternative : bool

use an alternative construction that is provably hard from resolution proofs.
Returns:
CNF

the CNF encoding for dominating of size \(\leq d\) for graph \(G\)
GraphAutomorphism(G)

Graph Automorphism formula

The formula is the CNF encoding of the statement that a graph G has a nontrivial automorphism, i.e. an automorphism different from the idential one.

Returns:
A CNF formula which is satiafiable if and only if graph G has a
nontrivial automorphism.
CountingPrinciple(M, p)

Generates the clauses for the counting matching principle.

The principle claims that there is a way to partition M in sets of size p each.

Arguments: - M : size of the domain - p : size of each class

BinaryCliqueFormula(G, k)

Test whether a graph has a k-clique.

Given a graph \(G\) and a non negative value \(k\), the CNF formula claims that \(G\) contains a \(k\)-clique. This formula uses the binary encoding, in the sense that the clique elements are indexed by strings of bits.

Parameters:
G : networkx.Graph

a simple graph

k : a non negative integer

clique size
Returns:
a CNF object
PerfectMatchingPrinciple(G)

Generates the clauses for the graph perfect matching principle.

The principle claims that there is a way to select edges to such that all vertices have exactly one incident edge set to 1.

Parameters:
G : undirected graph
TseitinFormula(graph, charges=None)

Build a Tseitin formula based on the input graph.

Odd charge is put on the first vertex by default, unless other vertices are is specified in input.

Arguments: - graph: input graph - `charges’: odd or even charge for each vertex

SparseStoneFormula(D, B)

Sparse Stone formulas

This is a variant of the StoneFormula(). See that for a description of the formula. This variant is such that each vertex has only a small selection of which stone can go to that vertex. In particular which stones are allowed on each vertex is specified by a bipartite graph \(B\) on which the left vertices represent the vertices of DAG \(D\) and the right vertices are the stones.

If a vertex of \(D\) correspond to the left vertex \(v\) in \(B\), then its neighbors describe which stones are allowed for it.

The vertices in \(D\) do not need to have the same name as the one on the left side of \(B\). It is only important that the number of vertices in \(D\) is the same as the vertices in the left side of \(B\).

In that case the element at position \(i\) in the ordered sequence enumerate_vertices(D) corresponds to the element of rank \(i\) in the sequence of left side vertices of \(B\) according to the output of Left, Right = bipartite_sets(B).

Standard StoneFormula() is essentially equivalent to a sparse stone formula where \(B\) is the complete graph.

Parameters:
D : a directed acyclic graph

it should be a directed acyclic graph.

B : bipartite graph
Raises:
ValueError

if \(D\) is not a directed acyclic graph

ValueError

if \(B\) is not a bipartite graph

ValueError

when size differs between \(D\) and the left side of \(B\)

See also

StoneFormula

CliqueColoring(n, k, c)

Clique-coloring CNF formula

The formula claims that a graph \(G\) with \(n\) vertices simultaneously contains a clique of size \(k\) and a coloring of size \(c\).

If \(k = c + 1\) then the formula is clearly unsatisfiable, and it is the only known example of a formula hard for cutting planes proof system. [1]

Variables \(e_{u,v}\) to encode the edges of the graph.

Variables \(q_{i,v}\) encode a function from \([k]\) to \([n]\) that represents a clique.

Variables \(r_{v,\ell}\) encode a function from \([n]\) to \([c]\) that represents a coloring.

Parameters:
n : number of vertices in the graph
k : size of the clique
c : size of the coloring
Returns:
A CNF object

References

[1](1, 2) Pavel Pudlak. Lower bounds for resolution and cutting plane proofs and monotone computations. Journal of Symbolic Logic (1997)
GraphPigeonholePrinciple(graph, functional=False, onto=False)

Graph Pigeonhole Principle CNF formula

The graph pigeonhole principle CNF formula, defined on a bipartite graph G=(L,R,E), claims that there is a subset E’ of the edges such that every vertex on the left size L has at least one incident edge in E’ and every edge on the right side R has at most one incident edge in E’.

This is possible only if the graph has a matching of size |L|.

There are different variants of this formula, depending on the values of functional and onto argument.

  • PHP(G): each left vertex can be incident to multiple edges in E’
  • FPHP(G): each left vertex must be incident to exaclty one edge in E’
  • onto-PHP: all right vertices must be incident to some vertex
  • matching: E’ must be a perfect matching between L and R

Arguments: - graph : bipartite graph - functional: add clauses to enforce at most one edge per left vertex - onto: add clauses to enforce that any right vertex has one incident edge

Remark: the graph vertices must have the ‘bipartite’ attribute set. Left vertices must have it set to 0 and the right ones to 1. A KeyException is raised otherwise.

RandomKCNF(k, n, m, seed=None, planted_assignments=[])

Build a random k-CNF

Sample \(m\) clauses over \(n\) variables, each of width \(k\), uniformly at random. The sampling is done without repetition, meaning that whenever a randomly picked clause is already in the CNF, it is sampled again.

Parameters:
k : int

width of each clause

n : int

number of variables to choose from. The resulting CNF object will contain n variables even if some are not mentioned in the clauses.

m : int

number of clauses to generate

seed : hashable object

seed of the random generator

planted_assignments : iterable(dict), optional

a set of total/partial assigments such that all clauses in the formula will be satisfied by all of them.
Returns:
a CNF object
Raises:
ValueError

when some paramenter is negative, or when k>n.
class MajoritySubstitution(cnf, rank)

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Transformed formula: substitutes variable with a Majority

Attributes:
header

Header getter

Methods

add_clause(clause[, literal_repetitions, …]) Add a clause to the CNF.
add_clause_unsafe(clause) Add a clause without checking input
add_variable(var[, description]) Add a variable to the formula (if not already resent).
binary_mapping(D, R, **kwargs) Binary CNF representation of a mapping between two sets.
clauses() Return the list of clauses
dimacs([export_header, extra_text]) Produce the dimacs encoding of the formula
equal_to_constraint(variables, value) Clauses encoding a “equal to” constraint
exactly_half_ceil(variables) Clauses encoding a “exactly half” constraint (rounded up)
exactly_half_floor(variables) Clauses encoding a “exactly half” constraint (rounded down)
greater_or_equal_constraint(variables, …) Clauses encoding a “greater than or equal to” constraint
greater_than_constraint(variables, lowerbound) Clauses encoding a “strictly greater than” constraint
is_satisfiable([cmd, sameas, verbose]) Determines whether a CNF is satisfiable or not.
latex([export_header, extra_text, full_document]) Output a LaTeX version of the CNF formula
less_or_equal_constraint(variables, upperbound) Clauses encoding a “less than or equal to” constraint
less_than_constraint(variables, upperbound) Clauses encoding a “strictly less than” constraint
loose_majority_constraint(variables) Clauses encoding a “at least half” constraint
loose_minority_constraint(variables) Clauses encoding a “at most half” constraint
parity_constraint(variables, constant) Output the CNF encoding of a parity constraint
transform_a_literal(polarity, varname) Substitute a positive literal with Loose Majority, and negative literals with Strict Minority.
transform_variable_preamble(name) Additional clauses for each variable
unary_mapping(D, R, **kwargs) Unary CNF representation of a mapping between two sets.
variables() Returns (a copy of) the list of variable names.
transform_a_literal(polarity, varname)

Substitute a positive literal with Loose Majority, and negative literals with Strict Minority.

Parameters:
polarity : bool

polarity of the literal

varname : string

variable to be substituted

Returns: a list of clauses
Shuffle(cnf, variable_permutation=None, clause_permutation=None, polarity_flip=None)

Reshuffle the given cnf. Returns a formula logically equivalent to the input with the following transformations applied in order:

1. Polarity flips. polarity_flip is a {-1,1}^n vector. If the i-th entry is -1, all the literals with the i-th variable change its sign.

2. Variable permutations. variable_permutation is a permutation of [vars(cnf)]. All the literals with the old i-th variable are replaced with the new i-th variable.

3. Clause permutations. clause_permutation is a permutation of [0..m-1]. The resulting clauses are reordered according to the permutation.

class OrSubstitution(cnf, rank)

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Transformed formula: substitutes variable with a OR

Attributes:
header

Header getter

Methods

add_clause(clause[, literal_repetitions, …]) Add a clause to the CNF.
add_clause_unsafe(clause) Add a clause without checking input
add_variable(var[, description]) Add a variable to the formula (if not already resent).
binary_mapping(D, R, **kwargs) Binary CNF representation of a mapping between two sets.
clauses() Return the list of clauses
dimacs([export_header, extra_text]) Produce the dimacs encoding of the formula
equal_to_constraint(variables, value) Clauses encoding a “equal to” constraint
exactly_half_ceil(variables) Clauses encoding a “exactly half” constraint (rounded up)
exactly_half_floor(variables) Clauses encoding a “exactly half” constraint (rounded down)
greater_or_equal_constraint(variables, …) Clauses encoding a “greater than or equal to” constraint
greater_than_constraint(variables, lowerbound) Clauses encoding a “strictly greater than” constraint
is_satisfiable([cmd, sameas, verbose]) Determines whether a CNF is satisfiable or not.
latex([export_header, extra_text, full_document]) Output a LaTeX version of the CNF formula
less_or_equal_constraint(variables, upperbound) Clauses encoding a “less than or equal to” constraint
less_than_constraint(variables, upperbound) Clauses encoding a “strictly less than” constraint
loose_majority_constraint(variables) Clauses encoding a “at least half” constraint
loose_minority_constraint(variables) Clauses encoding a “at most half” constraint
parity_constraint(variables, constant) Output the CNF encoding of a parity constraint
transform_a_literal(polarity, varname) Substitute a positive literal with an OR, and negative literals with its negation.
transform_variable_preamble(name) Additional clauses for each variable
unary_mapping(D, R, **kwargs) Unary CNF representation of a mapping between two sets.
variables() Returns (a copy of) the list of variable names.
transform_a_literal(polarity, varname)

Substitute a positive literal with an OR, and negative literals with its negation.

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

class NotAllEqualSubstitution(cnf, rank)

Bases: cnfformula.transformations.substitutions.AllEqualSubstitution

Transformed formula: substitutes variable with ‘not all equals’

Attributes:
header

Header getter

Methods

add_clause(clause[, literal_repetitions, …]) Add a clause to the CNF.
add_clause_unsafe(clause) Add a clause without checking input
add_variable(var[, description]) Add a variable to the formula (if not already resent).
binary_mapping(D, R, **kwargs) Binary CNF representation of a mapping between two sets.
clauses() Return the list of clauses
dimacs([export_header, extra_text]) Produce the dimacs encoding of the formula
equal_to_constraint(variables, value) Clauses encoding a “equal to” constraint
exactly_half_ceil(variables) Clauses encoding a “exactly half” constraint (rounded up)
exactly_half_floor(variables) Clauses encoding a “exactly half” constraint (rounded down)
greater_or_equal_constraint(variables, …) Clauses encoding a “greater than or equal to” constraint
greater_than_constraint(variables, lowerbound) Clauses encoding a “strictly greater than” constraint
is_satisfiable([cmd, sameas, verbose]) Determines whether a CNF is satisfiable or not.
latex([export_header, extra_text, full_document]) Output a LaTeX version of the CNF formula
less_or_equal_constraint(variables, upperbound) Clauses encoding a “less than or equal to” constraint
less_than_constraint(variables, upperbound) Clauses encoding a “strictly less than” constraint
loose_majority_constraint(variables) Clauses encoding a “at least half” constraint
loose_minority_constraint(variables) Clauses encoding a “at most half” constraint
parity_constraint(variables, constant) Output the CNF encoding of a parity constraint
transform_a_literal(polarity, varname) Substitute a positive literal with an ‘not all equal’ statement,
transform_variable_preamble(name) Additional clauses for each variable
unary_mapping(D, R, **kwargs) Unary CNF representation of a mapping between two sets.
variables() Returns (a copy of) the list of variable names.
transform_a_literal(polarity, varname)

Substitute a positive literal with an ‘not all equal’ statement,

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

class VariableCompression(cnf, B, function='xor')

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Vabiable compression transformation

The original variable are substituted with the XOR (or MAJ) of a subset of a new set of variables (usually smaller).

Attributes:
header

Header getter

Methods

add_clause(clause[, literal_repetitions, …]) Add a clause to the CNF.
add_clause_unsafe(clause) Add a clause without checking input
add_variable(var[, description]) Add a variable to the formula (if not already resent).
binary_mapping(D, R, **kwargs) Binary CNF representation of a mapping between two sets.
clauses() Return the list of clauses
dimacs([export_header, extra_text]) Produce the dimacs encoding of the formula
equal_to_constraint(variables, value) Clauses encoding a “equal to” constraint
exactly_half_ceil(variables) Clauses encoding a “exactly half” constraint (rounded up)
exactly_half_floor(variables) Clauses encoding a “exactly half” constraint (rounded down)
greater_or_equal_constraint(variables, …) Clauses encoding a “greater than or equal to” constraint
greater_than_constraint(variables, lowerbound) Clauses encoding a “strictly greater than” constraint
is_satisfiable([cmd, sameas, verbose]) Determines whether a CNF is satisfiable or not.
latex([export_header, extra_text, full_document]) Output a LaTeX version of the CNF formula
less_or_equal_constraint(variables, upperbound) Clauses encoding a “less than or equal to” constraint
less_than_constraint(variables, upperbound) Clauses encoding a “strictly less than” constraint
loose_majority_constraint(variables) Clauses encoding a “at least half” constraint
loose_minority_constraint(variables) Clauses encoding a “at most half” constraint
parity_constraint(variables, constant) Output the CNF encoding of a parity constraint
transform_a_literal(polarity, varname) Substitute a literal with a (negated) XOR
transform_variable_preamble(name) Additional clauses for each variable
unary_mapping(D, R, **kwargs) Unary CNF representation of a mapping between two sets.
variables() Returns (a copy of) the list of variable names.
transform_a_literal(polarity, varname)

Substitute a literal with a (negated) XOR

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

class IfThenElseSubstitution(cnf)

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Transformed formula: substitutes variable with a three variables if-then-else

Attributes:
header

Header getter

Methods

add_clause(clause[, literal_repetitions, …]) Add a clause to the CNF.
add_clause_unsafe(clause) Add a clause without checking input
add_variable(var[, description]) Add a variable to the formula (if not already resent).
binary_mapping(D, R, **kwargs) Binary CNF representation of a mapping between two sets.
clauses() Return the list of clauses
dimacs([export_header, extra_text]) Produce the dimacs encoding of the formula
equal_to_constraint(variables, value) Clauses encoding a “equal to” constraint
exactly_half_ceil(variables) Clauses encoding a “exactly half” constraint (rounded up)
exactly_half_floor(variables) Clauses encoding a “exactly half” constraint (rounded down)
greater_or_equal_constraint(variables, …) Clauses encoding a “greater than or equal to” constraint
greater_than_constraint(variables, lowerbound) Clauses encoding a “strictly greater than” constraint
is_satisfiable([cmd, sameas, verbose]) Determines whether a CNF is satisfiable or not.
latex([export_header, extra_text, full_document]) Output a LaTeX version of the CNF formula
less_or_equal_constraint(variables, upperbound) Clauses encoding a “less than or equal to” constraint
less_than_constraint(variables, upperbound) Clauses encoding a “strictly less than” constraint
loose_majority_constraint(variables) Clauses encoding a “at least half” constraint
loose_minority_constraint(variables) Clauses encoding a “at most half” constraint
parity_constraint(variables, constant) Output the CNF encoding of a parity constraint
transform_a_literal(polarity, varname) Substitute a positive literal with an if then else statement,
transform_variable_preamble(name) Additional clauses for each variable
unary_mapping(D, R, **kwargs) Unary CNF representation of a mapping between two sets.
variables() Returns (a copy of) the list of variable names.
transform_a_literal(polarity, varname)

Substitute a positive literal with an if then else statement,

Arguments: - polarity: polarity of the literal - varname: variable to be substituted

Returns: a list of clauses

class AllEqualSubstitution(cnf, rank)

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Transformed formula: substitutes variable with ‘all equals’

Attributes:
header

Header getter

Methods

add_clause(clause[, literal_repetitions, …]) Add a clause to the CNF.
add_clause_unsafe(clause) Add a clause without checking input
add_variable(var[, description]) Add a variable to the formula (if not already resent).
binary_mapping(D, R, **kwargs) Binary CNF representation of a mapping between two sets.
clauses() Return the list of clauses
dimacs([export_header, extra_text]) Produce the dimacs encoding of the formula
equal_to_constraint(variables, value) Clauses encoding a “equal to” constraint
exactly_half_ceil(variables) Clauses encoding a “exactly half” constraint (rounded up)
exactly_half_floor(variables) Clauses encoding a “exactly half” constraint (rounded down)
greater_or_equal_constraint(variables, …) Clauses encoding a “greater than or equal to” constraint
greater_than_constraint(variables, lowerbound) Clauses encoding a “strictly greater than” constraint
is_satisfiable([cmd, sameas, verbose]) Determines whether a CNF is satisfiable or not.
latex([export_header, extra_text, full_document]) Output a LaTeX version of the CNF formula
less_or_equal_constraint(variables, upperbound) Clauses encoding a “less than or equal to” constraint
less_than_constraint(variables, upperbound) Clauses encoding a “strictly less than” constraint
loose_majority_constraint(variables) Clauses encoding a “at least half” constraint
loose_minority_constraint(variables) Clauses encoding a “at most half” constraint
parity_constraint(variables, constant) Output the CNF encoding of a parity constraint
transform_a_literal(polarity, varname) Substitute a positive literal with an ‘all equal’ statement,
transform_variable_preamble(name) Additional clauses for each variable
unary_mapping(D, R, **kwargs) Unary CNF representation of a mapping between two sets.
variables() Returns (a copy of) the list of variable names.
transform_a_literal(polarity, varname)

Substitute a positive literal with an ‘all equal’ statement,

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

class FlipPolarity(cnf)

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Flip the polarity of variables

Attributes:
header

Header getter

Methods

add_clause(clause[, literal_repetitions, …]) Add a clause to the CNF.
add_clause_unsafe(clause) Add a clause without checking input
add_variable(var[, description]) Add a variable to the formula (if not already resent).
binary_mapping(D, R, **kwargs) Binary CNF representation of a mapping between two sets.
clauses() Return the list of clauses
dimacs([export_header, extra_text]) Produce the dimacs encoding of the formula
equal_to_constraint(variables, value) Clauses encoding a “equal to” constraint
exactly_half_ceil(variables) Clauses encoding a “exactly half” constraint (rounded up)
exactly_half_floor(variables) Clauses encoding a “exactly half” constraint (rounded down)
greater_or_equal_constraint(variables, …) Clauses encoding a “greater than or equal to” constraint
greater_than_constraint(variables, lowerbound) Clauses encoding a “strictly greater than” constraint
is_satisfiable([cmd, sameas, verbose]) Determines whether a CNF is satisfiable or not.
latex([export_header, extra_text, full_document]) Output a LaTeX version of the CNF formula
less_or_equal_constraint(variables, upperbound) Clauses encoding a “less than or equal to” constraint
less_than_constraint(variables, upperbound) Clauses encoding a “strictly less than” constraint
loose_majority_constraint(variables) Clauses encoding a “at least half” constraint
loose_minority_constraint(variables) Clauses encoding a “at most half” constraint
parity_constraint(variables, constant) Output the CNF encoding of a parity constraint
transform_a_literal(polarity, varname) Substitute a positive literal with an OR, and negative literals with its negation.
transform_variable_preamble(name) Additional clauses for each variable
unary_mapping(D, R, **kwargs) Unary CNF representation of a mapping between two sets.
variables() Returns (a copy of) the list of variable names.
transform_a_literal(polarity, varname)

Substitute a positive literal with an OR, and negative literals with its negation.

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

class ExactlyOneSubstitution(cnf, rank)

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Transformed formula: exactly one variable is true

Attributes:
header

Header getter

Methods

add_clause(clause[, literal_repetitions, …]) Add a clause to the CNF.
add_clause_unsafe(clause) Add a clause without checking input
add_variable(var[, description]) Add a variable to the formula (if not already resent).
binary_mapping(D, R, **kwargs) Binary CNF representation of a mapping between two sets.
clauses() Return the list of clauses
dimacs([export_header, extra_text]) Produce the dimacs encoding of the formula
equal_to_constraint(variables, value) Clauses encoding a “equal to” constraint
exactly_half_ceil(variables) Clauses encoding a “exactly half” constraint (rounded up)
exactly_half_floor(variables) Clauses encoding a “exactly half” constraint (rounded down)
greater_or_equal_constraint(variables, …) Clauses encoding a “greater than or equal to” constraint
greater_than_constraint(variables, lowerbound) Clauses encoding a “strictly greater than” constraint
is_satisfiable([cmd, sameas, verbose]) Determines whether a CNF is satisfiable or not.
latex([export_header, extra_text, full_document]) Output a LaTeX version of the CNF formula
less_or_equal_constraint(variables, upperbound) Clauses encoding a “less than or equal to” constraint
less_than_constraint(variables, upperbound) Clauses encoding a “strictly less than” constraint
loose_majority_constraint(variables) Clauses encoding a “at least half” constraint
loose_minority_constraint(variables) Clauses encoding a “at most half” constraint
parity_constraint(variables, constant) Output the CNF encoding of a parity constraint
transform_a_literal(polarity, varname) Substitute a literal with an “Exactly One”
transform_variable_preamble(name) Additional clauses for each variable
unary_mapping(D, R, **kwargs) Unary CNF representation of a mapping between two sets.
variables() Returns (a copy of) the list of variable names.
transform_a_literal(polarity, varname)

Substitute a literal with an “Exactly One”

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

class FormulaLifting(cnf, rank)

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Formula lifting: Y variable select X values

Attributes:
header

Header getter

Methods

add_clause(clause[, literal_repetitions, …]) Add a clause to the CNF.
add_clause_unsafe(clause) Add a clause without checking input
add_variable(var[, description]) Add a variable to the formula (if not already resent).
binary_mapping(D, R, **kwargs) Binary CNF representation of a mapping between two sets.
clauses() Return the list of clauses
dimacs([export_header, extra_text]) Produce the dimacs encoding of the formula
equal_to_constraint(variables, value) Clauses encoding a “equal to” constraint
exactly_half_ceil(variables) Clauses encoding a “exactly half” constraint (rounded up)
exactly_half_floor(variables) Clauses encoding a “exactly half” constraint (rounded down)
greater_or_equal_constraint(variables, …) Clauses encoding a “greater than or equal to” constraint
greater_than_constraint(variables, lowerbound) Clauses encoding a “strictly greater than” constraint
is_satisfiable([cmd, sameas, verbose]) Determines whether a CNF is satisfiable or not.
latex([export_header, extra_text, full_document]) Output a LaTeX version of the CNF formula
less_or_equal_constraint(variables, upperbound) Clauses encoding a “less than or equal to” constraint
less_than_constraint(variables, upperbound) Clauses encoding a “strictly less than” constraint
loose_majority_constraint(variables) Clauses encoding a “at least half” constraint
loose_minority_constraint(variables) Clauses encoding a “at most half” constraint
parity_constraint(variables, constant) Output the CNF encoding of a parity constraint
transform_a_literal(polarity, varname) Substitute a literal with a (negated) XOR
transform_variable_preamble(name) Additional clauses for each lifted variable
unary_mapping(D, R, **kwargs) Unary CNF representation of a mapping between two sets.
variables() Returns (a copy of) the list of variable names.
transform_a_literal(polarity, varname)

Substitute a literal with a (negated) XOR

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

transform_variable_preamble(name)

Additional clauses for each lifted variable

Arguments: - name: variable to be substituted

Returns: a list of clauses

class XorSubstitution(cnf, rank)

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Transformed formula: substitutes variable with a XOR

Attributes:
header

Header getter

Methods

add_clause(clause[, literal_repetitions, …]) Add a clause to the CNF.
add_clause_unsafe(clause) Add a clause without checking input
add_variable(var[, description]) Add a variable to the formula (if not already resent).
binary_mapping(D, R, **kwargs) Binary CNF representation of a mapping between two sets.
clauses() Return the list of clauses
dimacs([export_header, extra_text]) Produce the dimacs encoding of the formula
equal_to_constraint(variables, value) Clauses encoding a “equal to” constraint
exactly_half_ceil(variables) Clauses encoding a “exactly half” constraint (rounded up)
exactly_half_floor(variables) Clauses encoding a “exactly half” constraint (rounded down)
greater_or_equal_constraint(variables, …) Clauses encoding a “greater than or equal to” constraint
greater_than_constraint(variables, lowerbound) Clauses encoding a “strictly greater than” constraint
is_satisfiable([cmd, sameas, verbose]) Determines whether a CNF is satisfiable or not.
latex([export_header, extra_text, full_document]) Output a LaTeX version of the CNF formula
less_or_equal_constraint(variables, upperbound) Clauses encoding a “less than or equal to” constraint
less_than_constraint(variables, upperbound) Clauses encoding a “strictly less than” constraint
loose_majority_constraint(variables) Clauses encoding a “at least half” constraint
loose_minority_constraint(variables) Clauses encoding a “at most half” constraint
parity_constraint(variables, constant) Output the CNF encoding of a parity constraint
transform_a_literal(polarity, varname) Substitute a literal with a (negated) XOR
transform_variable_preamble(name) Additional clauses for each variable
unary_mapping(D, R, **kwargs) Unary CNF representation of a mapping between two sets.
variables() Returns (a copy of) the list of variable names.
transform_a_literal(polarity, varname)

Substitute a literal with a (negated) XOR

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses