cnfformula.cnf module¶

Build and manipulate CNF formulas

The module `contains facilities to generate cnf formulas, in order to be printed in DIMACS or LaTeX formats. Such formulas are ready to be fed to sat solvers.

The module implements the CNF object, which is the main entry point to the cnfformula library.

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.