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

None

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.

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

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.

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.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__()

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.