WCNF Formula

class optilog.formulas.WCNF(var_manager=None)

Creates an in-memory representation of a WCNF (Weighted Conjunctive Normal Form) formula.

hard_clauses: List[List[int]]: The list of all hard clauses in the formula.

soft_clauses: List[Tuple[int, List[int]]]: The list of all soft clauses in the formula.

sum_soft_weights()

Return type: Union[int, float]
Returns: The sum of all soft weights.

num_clauses()

Return type: int
Returns: The number of clauses (soft and hard) in the formula.

top_weight()

Return type: Union[int, float]
Returns: The weight for hard clauses = WCNF.sum_soft_weights + 1.

feasible(model)

Checks if a given assignment satisfies the hard constraints of a WCNF formula.

Parameters: assignment – A (possibly partial) assignment for the WCNF formula.
Return type: Optional[bool]
Returns: True/False (if the assignment satisfies or not) or None if some hard clause is undefined (notice that the assignment can be partial).

>>> wcnf = WCNF()
>>> wcnf.add_clauses([[1,2,3],[-1,-2],[-1,-3],[-2,-3]])
>>> wcnf.add_clauses([[-1], [-2]], weight=1)
>>> wcnf.feasible([-1,2,3])
>>> False
>>> wcnf.feasible([-1,-2,3])
>>> True
>>> wcnf = WCNF()
>>> wcnf.add_clauses([[1,2,3], [-1,-2]])
>>> wcnf.add_clauses([[-1]], weight=1)
>>> wcnf.feasible([3])
>>> 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: WCNF
Returns: A copy of the WCNF formula.

add_clauses(clauses, weight=0)

Adds a set of clauses of same weight to the WCNF formula. Extends variables if necessary.

Parameters

clause – The clause to be added to the formula.
weight (int) – If a weight is provided, the clause is considered as a soft clause. Notice that weights are always positive. If no weight is provided or weight = WCNF.INF_WEIGHT, the clause is considered as a hard clause.

>>> wcnf = WCNF()
>>> wcnf.add_clauses([[-1],[-2],[-3]], 1)
>>> wcnf.add_clauses([[1,2],[2,3]])
>>> print(wcnf)
p wcnf 3 5 4
c ===== Hard Clauses =====
4 1 2 0
4 2 3 0
c ===== Soft Clauses (Sum weights: 3) =====
1 -1 0
1 -2 0
1 -3 0

add_clause(clause, weight=0)

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

Parameters

clause (List[int]) – The clause to be added to the formula.
weight (int) – If a weight is provided, the clause is considered as a soft clause. Notice that weights are always positive. If no weight is provided or weight = WCNF.INF_WEIGHT, the clause is considered as a hard clause.

>>> wcnf = WCNF()
>>> wcnf.add_clause([1,2,3])
>>> wcnf.add_clause([1], 1)
>>> wcnf.add_clause([2], 1)
>>> wcnf.add_clause([3], 1)
>>> print(wcnf)
p wcnf 3 4 4
c ===== Hard Clauses =====
4 1 2 3 0
c ===== Soft Clauses (Sum weights: 3) =====
1 1 0
1 2 0
1 3 0

cost(assignment, inverse=False)

Parameters

assignment (List[int]) – A (possibly partial) assignment for the WCNF formula.
inverse (bool) – Inverse parameter.

Return type

Union[int, float]

Returns

Returns the aggregated weight of soft clauses violated or undefined by the assignment. If inverse parameter is True, returns the aggregated weight of the soft clauses satisfied by the assignment.

>>> wcnf = WCNF()
>>> wcnf.add_clause([1,2,3])
>>> wcnf.add_clauses([[-1],[-2],[-3]], 1)
>>> wcnf.cost([1,2])
3
>>> wcnf.cost([1,2], inverse=True)
0
>>> wcnf.cost([1,-2])
2
>>> wcnf.cost([1,-2], inverse=True)
1

write_dimacs(stream=<_io.TextIOWrapper name='<stdout>' mode='w' encoding='utf-8'>, format='classic')

Prints to the given stream the formula into DIMACS format.

Parameters

stream (IO) – The stream where to print the formula.
format – The wcnf format to output. Options are “classic” or “simplified”

write_dimacs_file(file_path, format='classic')

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

Parameters

file_path (str) – The file path where to write the formula.
format – The wcnf format to output. Options are “classic” or “simplified”

Return type

None

>>> cnf.write_dimacs_file('example')

shuffle(vars=True, soft_clauses=True, hard_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.
soft_clauses (bool) – Whether to shuffle the order of the soft_clauses of the formula.
hard_clauses (bool) – Whether to shuffle the order of the hard_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

>>> w = WCNF()
>>> w.add_clause([4,2,5])
>>> w.add_clause([4,5])
>>> w.add_clause([4,-2,3], weight=3)
>>> w.add_clause([4,-2,5], weight=5)
>>> w.hard_clauses
[[4, 2, 5], [4, 5]]
>>> w.soft_clauses
[(3, [4, -2, 3]), (5, [4, -2, 5])]
>>> w.shuffle()
>>> w.hard_clauses
[[1, 4, 5], [1, 5]]
>>> w.soft_clauses
[(5, [1, -4, 5]), (3, [1, -4, 2])]

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.

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.WCNFException: Invalid WCNF 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 WCNF
>>> wcnf = WCNF()
>>> wcnf.extend_vars(2)
>>> wcnf.max_var()
2
>>> wcnf.new_var()
3
>>> wcnf.max_var()
3
>>> wcnf.add_clause([1,2,3])
>>> wcnf.add_clauses([[1],[2],[3]], 1)
>>> wcnf.num_clauses()
4
>>> wcnf.soft_clauses
[(1, [1]), (1, [2]), (1, [3])]
>>> wcnf.hard_clauses
[1,2,3]
>>> wcnf.sum_soft_weights()
3
>>> wcnf.top_weight()
4
>>> wcnf.add_comment('a simple WCNF test formula')
>>> wcnf.header()
['a simple WCNF test formula']
>>> wcnf2 = wcnf.copy()
>>> wcnf2.soft_clauses, wcnf.hard_clauses
([(1, [1]), (1, [2]), (1, [3])], [[1, 2, 3]])
>>> wcnf2 = WCNF()
>>> wcnf2.max_var()
0
>>> wcnf2.soft_clauses, wcnf2.hard_clauses
([], [])

Methods sumary

Return type	Methods
int	`WCNF.new_var()`
int	`WCNF.max_var()`
list(str)	`WCNF.header()`
int	`WCNF.num_clauses()`
int or float	`WCNF.top_weight()`
None	`WCNF.extend_vars()`
None	`WCNF.set_minimum_vars()`
None	`WCNF.add_clause()`
None	`WCNF.add_clauses()`
bool or None	`WCNF.feasible()`
int or float	`WCNF.cost()`
None	`WCNF.add_comment()`
None	`WCNF.shuffle()`
None	`WCNF.write_dimacs()`
None	`WCNF.write_dimacs_file()`
WCNF	`WCNF.copy()`
str	`WCNF.__str__()`
str	`WCNF.__repr__()`