cnfgen.formula.basecnf module

The implementaton of the basic CNF object

class BaseCNF(clauses=None, description=None)

Bases: object

Basic 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_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=BaseCNF([[1, 2, -3], [-2, 4]])
>>> list(c)
[[1, 2, -3], [-2, 4]]
>>> c.add_clause([-3, 4, -5])
>>> list(c)
[[1, 2, -3], [-2, 4], [-3, 4, -5]]
>>> print(c[1])
[-2, 4]

Methods

add_clause(clause[, check])	Add a clause to the CNF.
add_clauses_from(clauses[, check])	Add a sequence of clauses to the CNF
all_variable_labels([default_label_format])	Produces the labels of all the variables
clauses()	Return the list of clauses
debug([allow_opposite, allow_repetition])	Check if the formula representation is correct
update_variable_number(new_value)	Raises the number of variable in the formula to new_value
variables()	Return the list of variables

number_of_clauses
number_of_variables

add_clause(clause, check=True)

Add a clause to the CNF.

E.g. (not x3) or x4 or (not x2) is encoded as [-1, 4, -2]

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.

By default no check is done on the clauses.

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.

check : bool

check that all literals as integer and update the number of variables, based on the literal present in the clause. (default: True)

add_clauses_from(clauses, check=True)

Add a sequence of clauses to the CNF

Parameters:

clause: list of clauses

the clauses to be added in the CNF

check : bool

check that all literals as integer and update the number of variables, based on the literal present in the clause. (default: False)

all_variable_labels(default_label_format='x{}')

Produces the labels of all the variables

clauses()

Return the list of clauses

debug(allow_opposite=False, allow_repetition=False)

Check if the formula representation is correct

Examples

>>> c=BaseCNF()
>>> c.add_clauses_from([[-1,2],[1,0,-2],[1,3]], check=False)
>>> c.debug()
False
>>> c=BaseCNF()
>>> c.add_clauses_from([[-1,2],[1,0,-2],[1,3]], check=True) # doctest: +IGNORE_EXCEPTION_DETAIL
Traceback (most recent call last):
ValueError: 0 is not a valid literal
>>> c=BaseCNF()
>>> c.add_clauses_from([[-1,2],[1,-2],[1,3]], check=False)
>>> c.debug()
False
>>> c=BaseCNF([[-1,2],[1,-2],[1,3]])
>>> c.debug()
True
>>> c.add_clause([-1,2,2])
>>> c.debug(allow_repetition=False)
False
>>> c.add_clause([3,2,-3])
>>> c.debug(allow_opposite=False)
False

number_of_clauses()

number_of_variables()

update_variable_number(new_value)

Raises the number of variable in the formula to new_value

If the formula has already at least new_value variables, this does not have any effect.

variables()

Return the list of variables

class ClausesView(F)

Bases: object

Object that represents a lit of clauses

Useful to provide some read only operations to the list of causes of a formula