QCNF Formula

class optilog.formulas.QCNF(var_manager=None)

num_clauses()

The number of clauses in the formula.

Return type

int

Returns

_description_

num_quant_levels()

Return type

int

Returns

The number of quantified levels within the QCNF formula.

property clauses: List[List[int]]

The list of all clauses 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.

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

set_minimum_vars(minimum)

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

Parameters

minimum (int) – The minimum number of variables this formula should have.

Return type

None

add_clause(clause)

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

Parameters

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

Return type

None

add_clauses(clauses)

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

Parameters

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

Return type

None

append_quant_set(quantifier, variables)

Appends a new set of quantified variables to the QCNF formula. Extends variables if necessary.

Parameters

• quantifier (str) – Quantifier of the variables; e for existential, a for universal.

• variables (List[int]) – Variables to be quantified.

Return type

None

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

QCNF

Returns

A copy of the QCNF formula.

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

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.

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

Invalid QCNF operation.

Creates an in-memory representation of a QCNF (Quantified Conjunctive Normal Form) formula.

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 QCNF
>>> qcnf = QCNF()
>>> qcnf.extend_vars(2)
>>> qcnf.max_var()
2
>>> qcnf.new_var()
3
>>> qcnf.max_var()
3
>>> qcnf.add_clauses([[1,2,3],[-1,-2],[-1,-3],[-2,-3]])
>>> qcnf.num_clauses()
4
>>> qcnf.clauses
[[1, 2, 3], [-1, -2], [-1, -3], [-2, -3]]
>>> qcnf.add_comment('a simple QCNF formula')
>>> qcnf.header()
['a simple QCNF formula']
>>> qcnf2 = QCNF()
>>> qcnf2.clauses
[]
>>> qcnf2.max_var()
0
>>> levels = [('a', [1, 2]), ('e', [3]), ('a', [4]), ('e', [5])]
>>> for quantifier, variables in levels:
>>>      qcnf2.append_quant_set(quantifier, variables)
>>> qcnf2.num_quant_levels()
4

Methods sumary

Return type	Methods
int	QCNF.new_var()
int	QCNF.max_var()
int	QCNF.max_var()
list(str)	QCNF.header()
int	QCNF.num_clauses()
int	QCNF.num_quant_levels()
None	QCNF.extend_vars()
None	QCNF.set_minimum_vars()
None	QCNF.add_clause()
None	QCNF.add_clauses()
None	QCNF.append_quant_set()
bool or None	QCNF.add_comment()
None	QCNF.write_dimacs()
QCNF	QCNF.copy()
QCNF	QCNF.__str__()
str	QCNF.__repr__()