cnfformula.transformations.substitutions module¶

class AllEqualSubstitution(cnf, rank)¶

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Transformed formula: substitutes variable with ‘all equals’

Attributes:	`header` Header getter

Methods

`add_clause`(clause[, literal_repetitions, …])	Add a clause to the CNF.
`add_clause_unsafe`(clause)	Add a clause without checking input
`add_variable`(var[, description])	Add a variable to the formula (if not already resent).
`binary_mapping`(D, R, **kwargs)	Binary CNF representation of a mapping between two sets.
`clauses`()	Return the list of clauses
`dimacs`([export_header, extra_text])	Produce the dimacs encoding of the formula
`equal_to_constraint`(variables, value)	Clauses encoding a “equal to” constraint
`exactly_half_ceil`(variables)	Clauses encoding a “exactly half” constraint (rounded up)
`exactly_half_floor`(variables)	Clauses encoding a “exactly half” constraint (rounded down)
`greater_or_equal_constraint`(variables, …)	Clauses encoding a “greater than or equal to” constraint
`greater_than_constraint`(variables, lowerbound)	Clauses encoding a “strictly greater than” constraint
`is_satisfiable`([cmd, sameas, verbose])	Determines whether a CNF is satisfiable or not.
`latex`([export_header, extra_text, full_document])	Output a LaTeX version of the CNF formula
`less_or_equal_constraint`(variables, upperbound)	Clauses encoding a “less than or equal to” constraint
`less_than_constraint`(variables, upperbound)	Clauses encoding a “strictly less than” constraint
`loose_majority_constraint`(variables)	Clauses encoding a “at least half” constraint
`loose_minority_constraint`(variables)	Clauses encoding a “at most half” constraint
`parity_constraint`(variables, constant)	Output the CNF encoding of a parity constraint
`transform_a_literal`(polarity, varname)	Substitute a positive literal with an ‘all equal’ statement,
`transform_variable_preamble`(name)	Additional clauses for each variable
`unary_mapping`(D, R, **kwargs)	Unary CNF representation of a mapping between two sets.
`variables`()	Returns (a copy of) the list of variable names.

transform_a_literal(polarity, varname)¶

Substitute a positive literal with an ‘all equal’ statement,

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

class AllEqualsSubstitutionCmd¶

Methods

setup_command_line
transform_cnf

description = 'substitute variable x with predicate x1==x2==...==xN (i.e. all equals)'¶

name = 'eq'¶

static setup_command_line(parser)¶

static transform_cnf(F, args)¶

class BaseSubstitution(cnf, new_variables=None)¶

Bases: cnfformula.cnf.CNF

Apply a substitution to a formula

Attributes:	`header` Header getter

Methods

`add_clause`(clause[, literal_repetitions, …])	Add a clause to the CNF.
`add_clause_unsafe`(clause)	Add a clause without checking input
`add_variable`(var[, description])	Add a variable to the formula (if not already resent).
`binary_mapping`(D, R, **kwargs)	Binary CNF representation of a mapping between two sets.
`clauses`()	Return the list of clauses
`dimacs`([export_header, extra_text])	Produce the dimacs encoding of the formula
`equal_to_constraint`(variables, value)	Clauses encoding a “equal to” constraint
`exactly_half_ceil`(variables)	Clauses encoding a “exactly half” constraint (rounded up)
`exactly_half_floor`(variables)	Clauses encoding a “exactly half” constraint (rounded down)
`greater_or_equal_constraint`(variables, …)	Clauses encoding a “greater than or equal to” constraint
`greater_than_constraint`(variables, lowerbound)	Clauses encoding a “strictly greater than” constraint
`is_satisfiable`([cmd, sameas, verbose])	Determines whether a CNF is satisfiable or not.
`latex`([export_header, extra_text, full_document])	Output a LaTeX version of the CNF formula
`less_or_equal_constraint`(variables, upperbound)	Clauses encoding a “less than or equal to” constraint
`less_than_constraint`(variables, upperbound)	Clauses encoding a “strictly less than” constraint
`loose_majority_constraint`(variables)	Clauses encoding a “at least half” constraint
`loose_minority_constraint`(variables)	Clauses encoding a “at most half” constraint
`parity_constraint`(variables, constant)	Output the CNF encoding of a parity constraint
`transform_a_literal`(polarity, name)	Substitute a literal with the transformation function
`transform_variable_preamble`(name)	Additional clauses for each variable
`unary_mapping`(D, R, **kwargs)	Unary CNF representation of a mapping between two sets.
`variables`()	Returns (a copy of) the list of variable names.

transform_a_literal(polarity, name)¶

Substitute a literal with the transformation function

Arguments: - polarity: polarity of the literal - name: variable to be substituted

Returns: a list of clauses

transform_variable_preamble(name)¶

Additional clauses for each variable

Arguments: - name: variable to add clauses for

Returns: a list of clauses

class ExactlyOneSubstitution(cnf, rank)¶

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Transformed formula: exactly one variable is true

Attributes:	`header` Header getter

Methods

`add_clause`(clause[, literal_repetitions, …])	Add a clause to the CNF.
`add_clause_unsafe`(clause)	Add a clause without checking input
`add_variable`(var[, description])	Add a variable to the formula (if not already resent).
`binary_mapping`(D, R, **kwargs)	Binary CNF representation of a mapping between two sets.
`clauses`()	Return the list of clauses
`dimacs`([export_header, extra_text])	Produce the dimacs encoding of the formula
`equal_to_constraint`(variables, value)	Clauses encoding a “equal to” constraint
`exactly_half_ceil`(variables)	Clauses encoding a “exactly half” constraint (rounded up)
`exactly_half_floor`(variables)	Clauses encoding a “exactly half” constraint (rounded down)
`greater_or_equal_constraint`(variables, …)	Clauses encoding a “greater than or equal to” constraint
`greater_than_constraint`(variables, lowerbound)	Clauses encoding a “strictly greater than” constraint
`is_satisfiable`([cmd, sameas, verbose])	Determines whether a CNF is satisfiable or not.
`latex`([export_header, extra_text, full_document])	Output a LaTeX version of the CNF formula
`less_or_equal_constraint`(variables, upperbound)	Clauses encoding a “less than or equal to” constraint
`less_than_constraint`(variables, upperbound)	Clauses encoding a “strictly less than” constraint
`loose_majority_constraint`(variables)	Clauses encoding a “at least half” constraint
`loose_minority_constraint`(variables)	Clauses encoding a “at most half” constraint
`parity_constraint`(variables, constant)	Output the CNF encoding of a parity constraint
`transform_a_literal`(polarity, varname)	Substitute a literal with an “Exactly One”
`transform_variable_preamble`(name)	Additional clauses for each variable
`unary_mapping`(D, R, **kwargs)	Unary CNF representation of a mapping between two sets.
`variables`()	Returns (a copy of) the list of variable names.

transform_a_literal(polarity, varname)¶

Substitute a literal with an “Exactly One”

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

class ExactlyOneSubstitutionCmd¶

Methods

setup_command_line
transform_cnf

description = 'substitute variable x with predicate x1+x2+...+xN = 1'¶

name = 'one'¶

static setup_command_line(parser)¶

static transform_cnf(F, args)¶

class FlipCmd¶

Methods

setup_command_line
transform_cnf

description = 'negate all variables in the formula'¶

name = 'flip'¶

static setup_command_line(parser)¶

static transform_cnf(F, args)¶

class FlipPolarity(cnf)¶

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Flip the polarity of variables

Attributes:	`header` Header getter

Methods

`add_clause`(clause[, literal_repetitions, …])	Add a clause to the CNF.
`add_clause_unsafe`(clause)	Add a clause without checking input
`add_variable`(var[, description])	Add a variable to the formula (if not already resent).
`binary_mapping`(D, R, **kwargs)	Binary CNF representation of a mapping between two sets.
`clauses`()	Return the list of clauses
`dimacs`([export_header, extra_text])	Produce the dimacs encoding of the formula
`equal_to_constraint`(variables, value)	Clauses encoding a “equal to” constraint
`exactly_half_ceil`(variables)	Clauses encoding a “exactly half” constraint (rounded up)
`exactly_half_floor`(variables)	Clauses encoding a “exactly half” constraint (rounded down)
`greater_or_equal_constraint`(variables, …)	Clauses encoding a “greater than or equal to” constraint
`greater_than_constraint`(variables, lowerbound)	Clauses encoding a “strictly greater than” constraint
`is_satisfiable`([cmd, sameas, verbose])	Determines whether a CNF is satisfiable or not.
`latex`([export_header, extra_text, full_document])	Output a LaTeX version of the CNF formula
`less_or_equal_constraint`(variables, upperbound)	Clauses encoding a “less than or equal to” constraint
`less_than_constraint`(variables, upperbound)	Clauses encoding a “strictly less than” constraint
`loose_majority_constraint`(variables)	Clauses encoding a “at least half” constraint
`loose_minority_constraint`(variables)	Clauses encoding a “at most half” constraint
`parity_constraint`(variables, constant)	Output the CNF encoding of a parity constraint
`transform_a_literal`(polarity, varname)	Substitute a positive literal with an OR, and negative literals with its negation.
`transform_variable_preamble`(name)	Additional clauses for each variable
`unary_mapping`(D, R, **kwargs)	Unary CNF representation of a mapping between two sets.
`variables`()	Returns (a copy of) the list of variable names.

transform_a_literal(polarity, varname)¶

Substitute a positive literal with an OR, and negative literals with its negation.

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

class FormulaLifting(cnf, rank)¶

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Formula lifting: Y variable select X values

Attributes:	`header` Header getter

Methods

`add_clause`(clause[, literal_repetitions, …])	Add a clause to the CNF.
`add_clause_unsafe`(clause)	Add a clause without checking input
`add_variable`(var[, description])	Add a variable to the formula (if not already resent).
`binary_mapping`(D, R, **kwargs)	Binary CNF representation of a mapping between two sets.
`clauses`()	Return the list of clauses
`dimacs`([export_header, extra_text])	Produce the dimacs encoding of the formula
`equal_to_constraint`(variables, value)	Clauses encoding a “equal to” constraint
`exactly_half_ceil`(variables)	Clauses encoding a “exactly half” constraint (rounded up)
`exactly_half_floor`(variables)	Clauses encoding a “exactly half” constraint (rounded down)
`greater_or_equal_constraint`(variables, …)	Clauses encoding a “greater than or equal to” constraint
`greater_than_constraint`(variables, lowerbound)	Clauses encoding a “strictly greater than” constraint
`is_satisfiable`([cmd, sameas, verbose])	Determines whether a CNF is satisfiable or not.
`latex`([export_header, extra_text, full_document])	Output a LaTeX version of the CNF formula
`less_or_equal_constraint`(variables, upperbound)	Clauses encoding a “less than or equal to” constraint
`less_than_constraint`(variables, upperbound)	Clauses encoding a “strictly less than” constraint
`loose_majority_constraint`(variables)	Clauses encoding a “at least half” constraint
`loose_minority_constraint`(variables)	Clauses encoding a “at most half” constraint
`parity_constraint`(variables, constant)	Output the CNF encoding of a parity constraint
`transform_a_literal`(polarity, varname)	Substitute a literal with a (negated) XOR
`transform_variable_preamble`(name)	Additional clauses for each lifted variable
`unary_mapping`(D, R, **kwargs)	Unary CNF representation of a mapping between two sets.
`variables`()	Returns (a copy of) the list of variable names.

transform_a_literal(polarity, varname)¶

Substitute a literal with a (negated) XOR

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

transform_variable_preamble(name)¶

Additional clauses for each lifted variable

Arguments: - name: variable to be substituted

Returns: a list of clauses

class FormulaLiftingCmd¶

Lifting

Methods

setup_command_line
transform_cnf

description = 'one dimensional lifting x --> x1 y1 OR ... OR xN yN, with y1+..+yN = 1'¶

name = 'lift'¶

static setup_command_line(parser)¶

static transform_cnf(F, args)¶

class IfThenElseSubstitution(cnf)¶

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Transformed formula: substitutes variable with a three variables if-then-else

Attributes:	`header` Header getter

Methods

`add_clause`(clause[, literal_repetitions, …])	Add a clause to the CNF.
`add_clause_unsafe`(clause)	Add a clause without checking input
`add_variable`(var[, description])	Add a variable to the formula (if not already resent).
`binary_mapping`(D, R, **kwargs)	Binary CNF representation of a mapping between two sets.
`clauses`()	Return the list of clauses
`dimacs`([export_header, extra_text])	Produce the dimacs encoding of the formula
`equal_to_constraint`(variables, value)	Clauses encoding a “equal to” constraint
`exactly_half_ceil`(variables)	Clauses encoding a “exactly half” constraint (rounded up)
`exactly_half_floor`(variables)	Clauses encoding a “exactly half” constraint (rounded down)
`greater_or_equal_constraint`(variables, …)	Clauses encoding a “greater than or equal to” constraint
`greater_than_constraint`(variables, lowerbound)	Clauses encoding a “strictly greater than” constraint
`is_satisfiable`([cmd, sameas, verbose])	Determines whether a CNF is satisfiable or not.
`latex`([export_header, extra_text, full_document])	Output a LaTeX version of the CNF formula
`less_or_equal_constraint`(variables, upperbound)	Clauses encoding a “less than or equal to” constraint
`less_than_constraint`(variables, upperbound)	Clauses encoding a “strictly less than” constraint
`loose_majority_constraint`(variables)	Clauses encoding a “at least half” constraint
`loose_minority_constraint`(variables)	Clauses encoding a “at most half” constraint
`parity_constraint`(variables, constant)	Output the CNF encoding of a parity constraint
`transform_a_literal`(polarity, varname)	Substitute a positive literal with an if then else statement,
`transform_variable_preamble`(name)	Additional clauses for each variable
`unary_mapping`(D, R, **kwargs)	Unary CNF representation of a mapping between two sets.
`variables`()	Returns (a copy of) the list of variable names.

transform_a_literal(polarity, varname)¶

Substitute a positive literal with an if then else statement,

Arguments: - polarity: polarity of the literal - varname: variable to be substituted

Returns: a list of clauses

class IfThenElseSubstitutionCmd¶

Methods

setup_command_line
transform_cnf

description = 'substitute variable x with predicate "if X then Y else Z"'¶

name = 'ite'¶

static setup_command_line(parser)¶

static transform_cnf(F, args)¶

class MajCompressionCmd¶

Methods

setup_command_line
transform_cnf

description = 'variable compression using Majority'¶

name = 'majcomp'¶

static setup_command_line(parser)¶

static transform_cnf(F, args)¶

class MajSubstitution¶

Methods

setup_command_line
transform_cnf

description = 'substitute variable x with predicate Majority(x1,x2,...,xN)'¶

name = 'maj'¶

static setup_command_line(parser)¶

static transform_cnf(F, args)¶

class MajoritySubstitution(cnf, rank)¶

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Transformed formula: substitutes variable with a Majority

Attributes:	`header` Header getter

Methods

`add_clause`(clause[, literal_repetitions, …])	Add a clause to the CNF.
`add_clause_unsafe`(clause)	Add a clause without checking input
`add_variable`(var[, description])	Add a variable to the formula (if not already resent).
`binary_mapping`(D, R, **kwargs)	Binary CNF representation of a mapping between two sets.
`clauses`()	Return the list of clauses
`dimacs`([export_header, extra_text])	Produce the dimacs encoding of the formula
`equal_to_constraint`(variables, value)	Clauses encoding a “equal to” constraint
`exactly_half_ceil`(variables)	Clauses encoding a “exactly half” constraint (rounded up)
`exactly_half_floor`(variables)	Clauses encoding a “exactly half” constraint (rounded down)
`greater_or_equal_constraint`(variables, …)	Clauses encoding a “greater than or equal to” constraint
`greater_than_constraint`(variables, lowerbound)	Clauses encoding a “strictly greater than” constraint
`is_satisfiable`([cmd, sameas, verbose])	Determines whether a CNF is satisfiable or not.
`latex`([export_header, extra_text, full_document])	Output a LaTeX version of the CNF formula
`less_or_equal_constraint`(variables, upperbound)	Clauses encoding a “less than or equal to” constraint
`less_than_constraint`(variables, upperbound)	Clauses encoding a “strictly less than” constraint
`loose_majority_constraint`(variables)	Clauses encoding a “at least half” constraint
`loose_minority_constraint`(variables)	Clauses encoding a “at most half” constraint
`parity_constraint`(variables, constant)	Output the CNF encoding of a parity constraint
`transform_a_literal`(polarity, varname)	Substitute a positive literal with Loose Majority, and negative literals with Strict Minority.
`transform_variable_preamble`(name)	Additional clauses for each variable
`unary_mapping`(D, R, **kwargs)	Unary CNF representation of a mapping between two sets.
`variables`()	Returns (a copy of) the list of variable names.

transform_a_literal(polarity, varname)¶

Substitute a positive literal with Loose Majority, and negative literals with Strict Minority.

Parameters:	polarity : bool polarity of the literal varname : string variable to be substituted Returns: a list of clauses

class NeqSubstitutionCmd¶

Methods

setup_command_line
transform_cnf

description = 'substitute variable x with predicate |{x1,x2,...,xN}|>1 (i.e. not all equals)'¶

name = 'neq'¶

static setup_command_line(parser)¶

static transform_cnf(F, args)¶

class NoSubstitutionCmd¶

Methods

setup_command_line
transform_cnf

description = 'no transformation'¶

name = 'none'¶

static setup_command_line(parser)¶

static transform_cnf(F, args)¶

class NotAllEqualSubstitution(cnf, rank)¶

Bases: cnfformula.transformations.substitutions.AllEqualSubstitution

Transformed formula: substitutes variable with ‘not all equals’

Attributes:	`header` Header getter

Methods

`add_clause`(clause[, literal_repetitions, …])	Add a clause to the CNF.
`add_clause_unsafe`(clause)	Add a clause without checking input
`add_variable`(var[, description])	Add a variable to the formula (if not already resent).
`binary_mapping`(D, R, **kwargs)	Binary CNF representation of a mapping between two sets.
`clauses`()	Return the list of clauses
`dimacs`([export_header, extra_text])	Produce the dimacs encoding of the formula
`equal_to_constraint`(variables, value)	Clauses encoding a “equal to” constraint
`exactly_half_ceil`(variables)	Clauses encoding a “exactly half” constraint (rounded up)
`exactly_half_floor`(variables)	Clauses encoding a “exactly half” constraint (rounded down)
`greater_or_equal_constraint`(variables, …)	Clauses encoding a “greater than or equal to” constraint
`greater_than_constraint`(variables, lowerbound)	Clauses encoding a “strictly greater than” constraint
`is_satisfiable`([cmd, sameas, verbose])	Determines whether a CNF is satisfiable or not.
`latex`([export_header, extra_text, full_document])	Output a LaTeX version of the CNF formula
`less_or_equal_constraint`(variables, upperbound)	Clauses encoding a “less than or equal to” constraint
`less_than_constraint`(variables, upperbound)	Clauses encoding a “strictly less than” constraint
`loose_majority_constraint`(variables)	Clauses encoding a “at least half” constraint
`loose_minority_constraint`(variables)	Clauses encoding a “at most half” constraint
`parity_constraint`(variables, constant)	Output the CNF encoding of a parity constraint
`transform_a_literal`(polarity, varname)	Substitute a positive literal with an ‘not all equal’ statement,
`transform_variable_preamble`(name)	Additional clauses for each variable
`unary_mapping`(D, R, **kwargs)	Unary CNF representation of a mapping between two sets.
`variables`()	Returns (a copy of) the list of variable names.

transform_a_literal(polarity, varname)¶

Substitute a positive literal with an ‘not all equal’ statement,

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

class OrSubstitution(cnf, rank)¶

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Transformed formula: substitutes variable with a OR

Attributes:	`header` Header getter

Methods

`add_clause`(clause[, literal_repetitions, …])	Add a clause to the CNF.
`add_clause_unsafe`(clause)	Add a clause without checking input
`add_variable`(var[, description])	Add a variable to the formula (if not already resent).
`binary_mapping`(D, R, **kwargs)	Binary CNF representation of a mapping between two sets.
`clauses`()	Return the list of clauses
`dimacs`([export_header, extra_text])	Produce the dimacs encoding of the formula
`equal_to_constraint`(variables, value)	Clauses encoding a “equal to” constraint
`exactly_half_ceil`(variables)	Clauses encoding a “exactly half” constraint (rounded up)
`exactly_half_floor`(variables)	Clauses encoding a “exactly half” constraint (rounded down)
`greater_or_equal_constraint`(variables, …)	Clauses encoding a “greater than or equal to” constraint
`greater_than_constraint`(variables, lowerbound)	Clauses encoding a “strictly greater than” constraint
`is_satisfiable`([cmd, sameas, verbose])	Determines whether a CNF is satisfiable or not.
`latex`([export_header, extra_text, full_document])	Output a LaTeX version of the CNF formula
`less_or_equal_constraint`(variables, upperbound)	Clauses encoding a “less than or equal to” constraint
`less_than_constraint`(variables, upperbound)	Clauses encoding a “strictly less than” constraint
`loose_majority_constraint`(variables)	Clauses encoding a “at least half” constraint
`loose_minority_constraint`(variables)	Clauses encoding a “at most half” constraint
`parity_constraint`(variables, constant)	Output the CNF encoding of a parity constraint
`transform_a_literal`(polarity, varname)	Substitute a positive literal with an OR, and negative literals with its negation.
`transform_variable_preamble`(name)	Additional clauses for each variable
`unary_mapping`(D, R, **kwargs)	Unary CNF representation of a mapping between two sets.
`variables`()	Returns (a copy of) the list of variable names.

transform_a_literal(polarity, varname)¶

Substitute a positive literal with an OR, and negative literals with its negation.

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

class OrSubstitutionCmd¶

Methods

setup_command_line
transform_cnf

description = 'substitute variable x with OR(x1,x2,...,xN)'¶

name = 'or'¶

static setup_command_line(parser)¶

static transform_cnf(F, args)¶

class VariableCompression(cnf, B, function='xor')¶

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Vabiable compression transformation

The original variable are substituted with the XOR (or MAJ) of a subset of a new set of variables (usually smaller).

Attributes:	`header` Header getter

Methods

`add_clause`(clause[, literal_repetitions, …])	Add a clause to the CNF.
`add_clause_unsafe`(clause)	Add a clause without checking input
`add_variable`(var[, description])	Add a variable to the formula (if not already resent).
`binary_mapping`(D, R, **kwargs)	Binary CNF representation of a mapping between two sets.
`clauses`()	Return the list of clauses
`dimacs`([export_header, extra_text])	Produce the dimacs encoding of the formula
`equal_to_constraint`(variables, value)	Clauses encoding a “equal to” constraint
`exactly_half_ceil`(variables)	Clauses encoding a “exactly half” constraint (rounded up)
`exactly_half_floor`(variables)	Clauses encoding a “exactly half” constraint (rounded down)
`greater_or_equal_constraint`(variables, …)	Clauses encoding a “greater than or equal to” constraint
`greater_than_constraint`(variables, lowerbound)	Clauses encoding a “strictly greater than” constraint
`is_satisfiable`([cmd, sameas, verbose])	Determines whether a CNF is satisfiable or not.
`latex`([export_header, extra_text, full_document])	Output a LaTeX version of the CNF formula
`less_or_equal_constraint`(variables, upperbound)	Clauses encoding a “less than or equal to” constraint
`less_than_constraint`(variables, upperbound)	Clauses encoding a “strictly less than” constraint
`loose_majority_constraint`(variables)	Clauses encoding a “at least half” constraint
`loose_minority_constraint`(variables)	Clauses encoding a “at most half” constraint
`parity_constraint`(variables, constant)	Output the CNF encoding of a parity constraint
`transform_a_literal`(polarity, varname)	Substitute a literal with a (negated) XOR
`transform_variable_preamble`(name)	Additional clauses for each variable
`unary_mapping`(D, R, **kwargs)	Unary CNF representation of a mapping between two sets.
`variables`()	Returns (a copy of) the list of variable names.

transform_a_literal(polarity, varname)¶

Substitute a literal with a (negated) XOR

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

class XorCompressionCmd¶

Methods

setup_command_line
transform_cnf

description = 'variable compression using XOR'¶

name = 'xorcomp'¶

static setup_command_line(parser)¶

static transform_cnf(F, args)¶

class XorSubstitution(cnf, rank)¶

Bases: cnfformula.transformations.substitutions.BaseSubstitution

Transformed formula: substitutes variable with a XOR

Attributes:	`header` Header getter

Methods

`add_clause`(clause[, literal_repetitions, …])	Add a clause to the CNF.
`add_clause_unsafe`(clause)	Add a clause without checking input
`add_variable`(var[, description])	Add a variable to the formula (if not already resent).
`binary_mapping`(D, R, **kwargs)	Binary CNF representation of a mapping between two sets.
`clauses`()	Return the list of clauses
`dimacs`([export_header, extra_text])	Produce the dimacs encoding of the formula
`equal_to_constraint`(variables, value)	Clauses encoding a “equal to” constraint
`exactly_half_ceil`(variables)	Clauses encoding a “exactly half” constraint (rounded up)
`exactly_half_floor`(variables)	Clauses encoding a “exactly half” constraint (rounded down)
`greater_or_equal_constraint`(variables, …)	Clauses encoding a “greater than or equal to” constraint
`greater_than_constraint`(variables, lowerbound)	Clauses encoding a “strictly greater than” constraint
`is_satisfiable`([cmd, sameas, verbose])	Determines whether a CNF is satisfiable or not.
`latex`([export_header, extra_text, full_document])	Output a LaTeX version of the CNF formula
`less_or_equal_constraint`(variables, upperbound)	Clauses encoding a “less than or equal to” constraint
`less_than_constraint`(variables, upperbound)	Clauses encoding a “strictly less than” constraint
`loose_majority_constraint`(variables)	Clauses encoding a “at least half” constraint
`loose_minority_constraint`(variables)	Clauses encoding a “at most half” constraint
`parity_constraint`(variables, constant)	Output the CNF encoding of a parity constraint
`transform_a_literal`(polarity, varname)	Substitute a literal with a (negated) XOR
`transform_variable_preamble`(name)	Additional clauses for each variable
`unary_mapping`(D, R, **kwargs)	Unary CNF representation of a mapping between two sets.
`variables`()	Returns (a copy of) the list of variable names.

transform_a_literal(polarity, varname)¶

Substitute a literal with a (negated) XOR

Arguments: - polarity: polarity of the literal - varname: fariable to be substituted

Returns: a list of clauses

class XorSubstitutionCmd¶

Methods

setup_command_line
transform_cnf

description = 'substitute variable x with XOR(x1,x2,...,xN)'¶

name = 'xor'¶

static setup_command_line(parser)¶

static transform_cnf(F, args)¶