cnfgen.formula.linear module¶

CNF formulas type with support of linear forms

This CNF formula type supports - linear equations mod 2 - integer linear inequalities on literals (no coefficients)

for example ‘atmost k’

class CNFLinear(clauses=None, description=None)¶

Bases: cnfgen.formula.basecnf.BaseCNF

CNF with linear constraints

Methods

`add_clause`(clause[, check])	Add a clause to the CNF.
`add_clauses_from`(clauses[, check])	Add a sequence of clauses to the CNF
`add_linear`(lits, op, constant[, check])	Add a linear constraint to the formula
`add_loose_majority`(lits[, check])	Clauses encoding a “at least half” constraint
`add_loose_minority`(lits[, check])	Clauses encoding a “at most half” constraint
`add_parity`(lits, constant[, check])	Adds the CNF encoding of a parity constraint
`add_strict_majority`(lits[, check])	Clauses encoding a “strict majority” constraint
`add_strict_minority`(lits[, check])	Clauses encoding a “at most half” constraint
`all_variable_labels`([default_label_format])	Produces the labels of all the variables
`clauses`()	Return the list of clauses
`debug`([allow_opposite, allow_repetition])	Check if the formula representation is correct
`update_variable_number`(new_value)	Raises the number of variable in the formula to new_value
`variables`()	Return the list of variables

number_of_clauses
number_of_variables

add_linear(lits, op, constant, check=True)¶

Add a linear constraint to the formula

Encodes an equality or an inequality constraint on literals (no coeffcients) as clauses.

Parameters:	lits : array-like literals op: str one among ‘<=’, “>=”, ‘<’, ‘>’, ‘==’, ‘!=’ constant : integer the constant of the linear equation check : bool check that the literals are valid and update the variable count Returns ——- None

Examples

>>> c = CNFLinear()
>>> c.add_linear([-1,2,-3],'>=',1)
>>> list(c)
[[-1, 2, -3]]
>>> c = CNFLinear()
>>> c.add_linear([-1,2,-3],'>=',3)
>>> list(c)
[[-1], [2], [-3]]
>>> c = CNFLinear()
>>> c.add_linear([-1,2,-3],'<',2)
>>> list(c)
[[1, -2], [1, 3], [-2, 3]]
>>> c = CNFLinear()
>>> c.add_linear([1,2,3],'<=',-1)
>>> list(c)
[[]]
>>> c = CNFLinear()
>>> c.add_linear([1,2,3],'<=',10)
>>> list(c)
[]

add_loose_majority(lits, check=True)¶

Clauses encoding a “at least half” constraint

Parameters:	lists : iterable(int) literals in the constraint check : bool check that the literals are valid and update the variable count

add_loose_minority(lits, check=True)¶

Clauses encoding a “at most half” constraint

Parameters:	lists : iterable(int) literals in the constraint check : bool check that the literals are valid and update the variable count

add_parity(lits, constant, check=True)¶

Adds the CNF encoding of a parity constraint

E.g. X1 + X2 + X3 = 1 (mod 2) is encoded as

( X1 v X2 v X3) (~X1 v ~X2 v X3) (~X1 v X2 v ~X3) ( X1 v ~X2 v ~X3)

Parameters:	variables : array-like literals constant : {0,1} the constant of the linear equation check : bool check that the literals are valid and update the variable count
Returns:	None

Examples

>>> C=CNFLinear()
>>> C.add_parity([-1,2],1)
>>> list(C)
[[-1, 2], [1, -2]]
>>> C=CNFLinear()
>>> C.add_parity([-1,2],0)
>>> list(C)
[[-1, -2], [1, 2]]

add_strict_majority(lits, check=True)¶

Clauses encoding a “strict majority” constraint

Parameters:	lists : iterable(int) literals in the constraint check : bool check that the literals are valid and update the variable count

add_strict_minority(lits, check=True)¶

Clauses encoding a “at most half” constraint

Parameters:	lists : iterable(int) literals in the constraint check : bool check that the literals are valid and update the variable count