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.

 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
10>>> wcnf.add_clause([1,2,3])
11>>> wcnf.add_clauses([[1],[2],[3]], 1)
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')
23>>> wcnf.header()
24['a simple WCNF test formula']
25>>> wcnf2 = wcnf.copy()
26>>> wcnf2.soft_clauses, wcnf.hard_clauses
27([(1, [1]), (1, [2]), (1, [3])], [[1, 2, 3]])
28>>> wcnf2 = WCNF()
29>>> wcnf2.max_var()
300
31>>> wcnf2.soft_clauses, wcnf2.hard_clauses
32([], [])

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