# 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.feasible([-1,2,3])
>>> False
>>> wcnf.feasible([-1,-2,3])
>>> True
>>> wcnf = WCNF()
>>> 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.

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()
>>> 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
```

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()
>>> 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.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.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])]
```

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`

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.

``` 1>>> from optilog.formulas import WCNF
2>>> wcnf = WCNF()
3>>> wcnf.extend_vars(2)
4>>> wcnf.max_var()
52
6>>> wcnf.new_var()
73
8>>> wcnf.max_var()
93
12>>> wcnf.num_clauses()
134
14>>> wcnf.soft_clauses
15[(1, [1]), (1, [2]), (1, [3])]
16>>> wcnf.hard_clauses
17[1,2,3]
18>>> wcnf.sum_soft_weights()
193
20>>> wcnf.top_weight()
214
22>>> wcnf.add_comment('a simple WCNF test formula')