class optilog.formulas.VarManager

A VarManager represents a pool of variables for a specific problem. It can be used to create variables and to keep track of the ones already created. Each variable created by a VarManager is assigned an identifier according to the DIMACS format, starting at 1.

The VarManager class is used by CNF, WCNF, and QCNF formulas.

copy()

Return type: VarManager
Returns: A copy of the VarManager

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_var(lit)

Creates a new DIMACS variable and associates it to the Expression.

Used to connect variables created with the Modelling module with an existing variable pool.

Parameters: lit (Expression) – The expression to associate
Return type: int
Returns: The associated DIMACS literal

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.

get_lit(lit, insert=True)

Returns the DIMACS literal associated with the Expression.

The lit parameter can be either an instance of a Bool, or its negation (an instance of a Not(Bool) expression). It also accepts nested negations, as long as the last element of the tree is a Bool. If the argument insert is True and no DIMACS literal is associated with the Expression, a new literal is created and associated.

Parameters

lit (Expression) – The expression to lookup
insert (bool) – Whether to create a new variable if the Expression has not been found.

Raises

ValueError – if the expression is not unitary
KeyError – if the literal is not found and the parameter insert is set to False

Return type

int

Returns

The associated DIMACS literal

Methods sumary

Return type	Methods
int	`VarManager.new_var()`
int	`VarManager.add_var()`
int	`VarManager.get_lit()`
int	`VarManager.max_var()`
None	`VarManager.extend_vars()`
None	`VarManager.set_minimum_vars()`

Example on how to use a VarManager:

>>> from optilog.formulas import VarManager, CNF
>>> v = VarManager()
>>> c1 = CNF(var_manager=v)
>>> c2 = CNF(var_manager=v)
>>> c1.new_var()
1
>>> c2.new_var()
2
>>> c1.new_var()
3
>>> v.new_var()
4
>>> from optilog.modelling import Bool, Not
>>> b1 = Bool('b1')
>>> v.add_var(b1)
5
>>> v.new_var()
6
>>> v.get_lit(b1)
5
>>> v.get_lit(Not(b1))
-5
>>> b2 = Bool('b2')
>>> v.get_lit(b2)
7
>>> v.decode_dimacs([-5,7])
[~b1, b2]

You may also assume implicit initialization of the VarManager and reuse it across objects:

>>> c1 = CNF()
>>> c1.new_var()
1
>>> c2 = CNF(var_manager=c1.var_manager)
>>> c1.new_var()
2
>>> c2.new_var()
3

All of these examples would be exactly equivalent with CNF/WCNF/QCNF.