# 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. :param assignment: A (possibly partial) assignment for the WCNF formula. :rtype: `Optional`[`bool`] :return: 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()
>>> 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
```
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

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

`None`

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`

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 WCNF
>>> wcnf = WCNF()
>>> wcnf.extend_vars(2)
>>> wcnf.max_var()
2
>>> wcnf.new_var()
3
>>> wcnf.max_var()
3
>>> wcnf.num_clauses()
4
>>> wcnf.soft_clauses
[(1, ), (1, ), (1, )]
>>> wcnf.hard_clauses
[1,2,3]
>>> wcnf.sum_soft_weights()
3
>>> wcnf.top_weight()
4
>>> wcnf.add_comment('a simple WCNF test formula')
['a simple WCNF test formula']
>>> wcnf2 = wcnf.copy()
>>> wcnf2.soft_clauses, wcnf.hard_clauses
([(1, ), (1, ), (1, )], [[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__()`

Footnotes

1

Solvers for weighted (partial) MaxSAT commonly use an extended DIMACS format for CNFs. In particular, this format adds weights to each clause and a way to specify hard constraints (for partial MaxSAT). This extended format is used and described by MaxSAT competitions requirements.