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

>>> 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]]
Return type

None

statistics()

Computes:

  • int: The number of variables

  • 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.

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

None

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'>)

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)

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

Parameters

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

>>> cnf.write_dimacs_file('example')
Return type

None

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.

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.