CNF Formula

class optilog.formulas.CNF(var_manager=None)

Creates an in-memory representation of a CNF (Conjunctive Normal Form) formula using the DIMACS 1 format.

DIMACS format defines that variables start at 1, and their negation is the negative value (e.g -1).

clauses: List[List[int]]

The list of all clauses in the formula.

num_clauses()

Return type

int

Returns

The number of clauses in the formula.

satisfied(model)

Checks if a given assignment satisfies the CNF formula.

Parameters

model (List[int]) – A (possibly partial) assignment for the CNF formula.

Return type

Optional[bool]

Returns

True/False (if the assignment satisfies or not) or None if some clause is undefined (notice that the assignment can be partial).

>>> cnf.clauses
[[1,2,3],[-1,-2],[-1,-3],[-2,-3]]
>>> cnf.satisfied([-1,2,3])
False
>>> cnf.satisfied([-1,-2,3])
True

copy()

Makes a deep copy of the formula object and returns it. Note that these two objects do not share any information after the copy has been done.

Return type

CNF

Returns

A copy of the CNF formula.

add_clauses(clauses)

Adds a set of clauses to the CNF formula. Extends variables if necessary.

Parameters

clauses (List[List[int]]) – The clauses to be added to the CNF formula.

Return type

None

add_clause(clause)

Adds a new clause to the CNF formula. Extends variables if necessary.

Parameters

clause (List[int]) – The clause to be added to the CNF formula.

Return type

None

shuffle(vars=True, clauses=True, literals=True, polarity=True, seed=None)

Shuffles the variables, clauses, literals and polarity of the formula. This may be used to test the performance of encodings on a formula.

Parameters

• vars (bool) – Whether to shuffle the variables of the formula.

• clauses (bool) – Whether to shuffle the order of the clauses of the formula.

• literals (bool) – Whether to shuffle the order of the literals of the clauses.

• polarity (bool) – Whether to shuffle the order of the polarity of the variables.

• seed (Optional[int]) – Optional seed for the shuffle

Return type

None

>>> from optilog.formulas import CNF
>>> c = CNF()
>>> c.add_clause([4,2,5])
>>> c.add_clause([4,2])
>>> c.add_clause([4])
>>> c.clauses
>>> [[4, 2, 5], [4, 2], [4]]
>>> c.shuffle(vars=True, clauses=False)
>>> c.clauses
>>> [[3, 1, 2], [3, 1], [3]]
>>> c.shuffle(vars=False, clauses=True)
>>> c.clauses
>>> [[3, 1], [3], [3, 1, 2]]

statistics()

Computes:

• int: The number of variables

• int: The maximum of variable

• int: Number of clauses of the formula

• [(size, frequency)] The number of clauses by size

• [(var, positive frequency, negative frequency)] The frequency of the variables

• int: The number of literals.

Return type

dict

Returns

Statistics of the formula

>>> from optilog.formulas import CNF
>>> c = CNF()
>>> c.add_clause([2,3,8])
>>> c.add_clause([10,3,1])
>>> c.statistics()
{'n_vars': 10, 'n_clauses': 2, 'clauses_by_size': [(3, 2)], 'frequency': [(1, 1, 0), (2, 1, 0), (3, 2, 0), (8, 1, 0), (10, 1, 0)], 'n_lits': 6}

add_comment(comment)

Adds a comment to the header of the formula. These comments will be displayed in the DIMACS format with the character c prepended, hence the DIMACS parser will ignore them.

Parameters

comment (Union[str, List[str]]) – Comment to append to the header.

Return type

None

>>> form.add_comment('a simple test formula')

extend_vars(how_many)

Creates a set of variables at once.

Parameters

how_many (int) – The number of variables to be created.

Return type

None

header()

Return type

List[str]

Returns

A list of strings representing comments on the formula.

max_var()

Return type

int

Returns

The maximum DIMACS variable id in the formula.

new_var()

Creates a new variable and returns its DIMACS id. The returned value will be max_var() + 1.

Return type

int

Returns

The newly created variable.

set_minimum_vars(minimum)

Creates a set of variables at once if the passed minimum number is bigger than the existing one.

Parameters

minimum – The minimum number of variables this formula should have.

write_dimacs(stream=<_io.TextIOWrapper name='<stdout>' mode='w' encoding='utf-8'>, *args, **kwargs)

Prints to the given stream the formula into DIMACS format.

Parameters

stream (IO) – The stream where to print the formula.

write_dimacs_file(file_path, *args, **kwargs)

Writes to the given file path the formula into DIMACS format.

Parameters

file_path (str) – The file path where to write the formula.

Return type

None

>>> cnf.write_dimacs_file('example')

var_manager: VarManager

This attribute allows formulas to share the same pool of variables. This can be used to represent a single problem with multiple partial formulas. See the reference documentation on the VarManager section for more information.

class optilog.formulas.CNFException

Invalid CNF operation.

An instance of VarManager can be provided though the parameter var_manager. This allows formulas to share the same pool of variables.

>>> from optilog.formulas import CNF
>>> cnf = CNF()
>>> cnf.extend_vars(2)
>>> cnf.max_var()
2
>>> cnf.new_var()
3
>>> cnf.max_var()
3
>>> cnf.add_clause([1,2,3])
>>> cnf.num_clauses()
1
>>> cnf.add_clauses([[-1,-2],[-1,-3],[-2,-3]])
>>> cnf.num_clauses()
4
>>> cnf.clauses
[[1,2,3],[-1,-2],[-1,-3],[-2,-3]]
>>> cnf.add_comment('a simple test formula')
>>> cnf.header()
['a simple test formula']
>>> cnf2 = cnf.copy()
>>> cnf2.clauses
[[1,2,3],[-1,-2],[-1,-3],[-2,-3]]

Methods sumary

Return type	Methods
int	CNF.new_var()
int	CNF.max_var()
list(str)	CNF.header()
int	CNF.num_clauses()
None	CNF.extend_vars()
None	CNF.set_minimum_vars()
None	CNF.add_clause()
None	CNF.add_clauses()
bool or None	CNF.satisfies()
None	CNF.add_comment()
None	CNF.shuffle()
None	CNF.write_dimacs()
None	CNF.write_dimacs_file()
CNF	CNF.copy()
Dict	CNF.statistics()
str	CNF.__str__()
str	CNF.__repr__()

Footnotes

1

SAT solvers commonly use the DIMACS format for CNFs. This format is used by SAT competitions requirements as originally described in DIMACS CNF suggested format.