API Reference

paramita.containers module

ClauseContainer

Bases: Plugin

A container of clauses.

The variables used in this container are represented as an integer larger than 0 (its identifier), as in the DIMACS CNF format.

A clause is composed by literals, which are a variable or its negation. A negated variable is represented by negating its identifier.

This interface acts as a clause container, in the sense that we can add new clauses and (optionally) keep track on how many clauses we added. No additional assumptions are made on how the container stores them (or even if they are stored at all). Specializations of this interface might provide additional methods to retrieve clauses, but this is not part of the interface.

add_clause

add_clause(clause)

Add a single clause.

The clause is represented as a sequence of literals. Each literal is represented as an integer, where its absolut value is the identifier of a variable. A positive integer represents the variable and a negative integer its negation.

Parameters:

Name	Type	Description	Default
clause	Sequence[int]	The clause to be added to the container.	required

add_clauses

add_clauses(clauses)

Add multiple clauses to the container.

The default implementation will call add_clause once per element in the vector.

Parameters:

Name	Type	Description	Default
clauses	Sequence[Sequence[int]]	The clauses to be added to the container.	required

add_lit

add_lit(lit)

Add a clause literal by literal.

This method is intended to be used to add clauses literal by literal. To insert a clause, call add_lit with each literal for the clause, and then commit the clause to the container by using add_lit(0).

See BALYO201645 for more details.

Parameters:

Name	Type	Description	Default
lit	int	The next literal for the current clause being added, or 0 to indicate the end of the clause.	required

clone

clone()

Clones the current CNF Container.

Returns:

Type	Description
ClauseContainer	The cloned CNF Container.

get

get(name)

Get the parameter's value.

Parameters:

Name	Type	Description	Default
name	str	The name of the parameter.	required

Returns:

Type	Description
str | int | float | bool | SatSolver | NonIncrSatSolver | ClauseContainer | NonIncrMaxSatSolver | WClauseContainer | PbToCnfEncoder | Plugin	The value of the parameter.

get_parameter_space

get_parameter_space()

Get the parameter space for this class.

Returns:

Type	Description
ParameterSpace	The parameter space.

max_var

max_var()

Get the largest variable used by the container.

The largest variable is determined by its identifier.

Returns:

Type	Description
int	The (positive) integer representing the largest variable.

num_clauses

num_clauses()

Get the number of clauses hold currently by the container.

This method returns the number of clauses that the container currently holds. It is implementation defined, meaning that it does not need to match the number of times that add_clause was called. For example, a simplification could be performed on the clauses, eliminating some of them.

Returns:

Type	Description
int	The number of clauses held by the container.

set

set(name, value)

Set a parameter.

Parameters:

Name	Type	Description	Default
name	str	The name of the parameter.	required
value	str | int | float | bool | SatSolver | NonIncrSatSolver | ClauseContainer | NonIncrMaxSatSolver | WClauseContainer | PbToCnfEncoder | Plugin	The value to set the parameter to.	required

set_minimum_var

set_minimum_var(var)

Sets the maximum variable known to the container to at least this one.

This method can be used to ensure that the container knows a certain variable. If the container internally generates new variables, or if someone relies on the method to determine the next free variable, this method ensures that existing variables cannot be reused.

Parameters:

Name	Type	Description	Default
var	int	The variable to be registered to the container.	required

CnfFormula

Bases: ClauseContainer

This class represents a boolean Conjunctive Normal Form (CNF) formula in the DIMACS format.

add_clause

add_clause(clause)

Add a single clause.

The clause is represented as a sequence of literals. Each literal is represented as an integer, where its absolut value is the identifier of a variable. A positive integer represents the variable and a negative integer its negation.

Parameters:

Name	Type	Description	Default
clause	Sequence[int]	The clause to be added to the container.	required

add_clauses

add_clauses(clauses)

Add multiple clauses to the container.

The default implementation will call add_clause once per element in the vector.

Parameters:

Name	Type	Description	Default
clauses	Sequence[Sequence[int]]	The clauses to be added to the container.	required

add_lit

add_lit(lit)

Add a clause literal by literal.

This method is intended to be used to add clauses literal by literal. To insert a clause, call add_lit with each literal for the clause, and then commit the clause to the container by using add_lit(0).

See BALYO201645 for more details.

Parameters:

Name	Type	Description	Default
lit	int	The next literal for the current clause being added, or 0 to indicate the end of the clause.	required

clauses

clauses()

Get the clauses in the formula.

clone

clone()

Clones the current CNF Container.

Returns:

Type	Description
ClauseContainer	The cloned CNF Container.

is_feasible

is_feasible(assignment)

Checks if a given (possibly partial) assignment is feasible.

Parameters:

Name	Type	Description	Default
assignment	Sequence[int]	The assignment to check.	required

Returns:

Type	Description
bool | None	True if the assignment is feasible, False if not,
bool | None	and None if the assignment is partial and could not
bool | None	determine if it is feasible or not.

max_var

max_var()

Get the largest variable used by the container.

The largest variable is determined by its identifier.

Returns:

Type	Description
int	The (positive) integer representing the largest variable.

num_clauses

num_clauses()

Get the number of clauses hold currently by the container.

This method returns the number of clauses that the container currently holds. It is implementation defined, meaning that it does not need to match the number of times that add_clause was called. For example, a simplification could be performed on the clauses, eliminating some of them.

Returns:

Type	Description
int	The number of clauses held by the container.

set_minimum_var

set_minimum_var(var)

Sets the maximum variable known to the container to at least this one.

This method can be used to ensure that the container knows a certain variable. If the container internally generates new variables, or if someone relies on the method to determine the next free variable, this method ensures that existing variables cannot be reused.

Parameters:

Name	Type	Description	Default
var	int	The variable to be registered to the container.	required

WClauseContainer

Bases: Plugin

A container of weighted clauses. A clause is a multiset of literals.

add_clause

add_clause(clause, weight=SPECIAL_WEIGHTS.TOP_WEIGHT)

Add a single clause with the specified weight.

Parameters:

Name	Type	Description	Default
clause	Sequence[int]	The clause to be added to the container.	required
weight	int | SPECIAL_WEIGHTS	The associated weight for this clause.	TOP_WEIGHT

add_clauses

add_clauses(clauses, weight=SPECIAL_WEIGHTS.TOP_WEIGHT)

Add multiple clauses to the container.

Parameters:

Name	Type	Description	Default
clauses	Sequence[Sequence[int]]	The clauses to be added to the container.	required
weight	int | SPECIAL_WEIGHTS	The associated weight for the clauses.	TOP_WEIGHT

add_lit

add_lit(lit)

Add a clause literal by literal.

This method is intended to be used to add clauses literal by literal. To insert a clause, call add_lit with each literal for the clause, and then commit the clause to the container by using add_lit(0).

See ipamir2022 and BALYO201645 for more details.

Parameters:

Name	Type	Description	Default
lit	int	The next literal for the current clause being added, or 0 to indicate the end of the clause.	required

add_soft_lit

add_soft_lit(lit, weight)

Declare a literal as a soft literal with a weight.

This function declares a literal as a soft literal in the underlying MaxSAT formula. Assigning the literal to true incurs cost weight.

If the literal is already set in the formula, this overrides the previous cost the literal had.

See ipamir2022 for more details.

Parameters:

Name	Type	Description	Default
lit	int	The soft literal.	required
weight	int	The new weight for the literal.	required

add_weight

add_weight(weight)

Changes the weight for the next clause that is added literal by literal.

Parameters:

Name	Type	Description	Default
weight	int | SPECIAL_WEIGHTS	The weight for the next clause.	required

clone

clone()

Clones the current container.

Returns:

Type	Description
WClauseContainer	The cloned container.

get

get(name)

Get the parameter's value.

Parameters:

Name	Type	Description	Default
name	str	The name of the parameter.	required

Returns:

Type	Description
str | int | float | bool | SatSolver | NonIncrSatSolver | ClauseContainer | NonIncrMaxSatSolver | WClauseContainer | PbToCnfEncoder | Plugin	The value of the parameter.

get_parameter_space

get_parameter_space()

Get the parameter space for this class.

Returns:

Type	Description
ParameterSpace	The parameter space.

max_var

max_var()

Get the largest variable used in the container.

Returns:

Type	Description
int	The (positive) integer assigned to the largest variable.

num_clauses

num_clauses()

Obtain the distribution of clauses hold by the container over weights.

This method returns the number of clauses that the container currently holds. It is implementation defined, meaning that it does not need to match the number of times that add_clause was called. For example, a simplification could be performed on the clauses, eliminating some of them.

Returns:

Type	Description
dict[int | SPECIAL_WEIGHTS, int]	The map with the distribution of clauses.

set

set(name, value)

Set a parameter.

Parameters:

Name	Type	Description	Default
name	str	The name of the parameter.	required
value	str | int | float | bool | SatSolver | NonIncrSatSolver | ClauseContainer | NonIncrMaxSatSolver | WClauseContainer | PbToCnfEncoder | Plugin	The value to set the parameter to.	required

set_minimum_var

set_minimum_var(var)

Sets the maximum variable known to the container to at least this one.

This method can be used to ensure that the container knows a certain variable. If the container internally generates new variables, or if someone relies on the method to determine the next free variable, this method ensures that existing variables cannot be reused.

Parameters:

Name	Type	Description	Default
var	int	The variable to be registered to the container.	required

WcnfFormula

Bases: WClauseContainer

This class represents a weighted boolean Conjunctive Normal Form (WCNF) formula in the DIMACS format.

add_clause

add_clause(clause, weight=SPECIAL_WEIGHTS.TOP_WEIGHT)

Add a single clause with the specified weight.

Parameters:

Name	Type	Description	Default
clause	Sequence[int]	The clause to be added to the container.	required
weight	int | SPECIAL_WEIGHTS	The associated weight for this clause.	TOP_WEIGHT

add_clauses

add_clauses(clauses, weight=SPECIAL_WEIGHTS.TOP_WEIGHT)

Add multiple clauses to the container.

Parameters:

Name	Type	Description	Default
clauses	Sequence[Sequence[int]]	The clauses to be added to the container.	required
weight	int | SPECIAL_WEIGHTS	The associated weight for the clauses.	TOP_WEIGHT

add_lit

add_lit(lit)

Add a clause literal by literal.

This method is intended to be used to add clauses literal by literal. To insert a clause, call add_lit with each literal for the clause, and then commit the clause to the container by using add_lit(0).

See ipamir2022 and BALYO201645 for more details.

Parameters:

Name	Type	Description	Default
lit	int	The next literal for the current clause being added, or 0 to indicate the end of the clause.	required

add_soft_lit

add_soft_lit(lit, weight)

Declare a literal as a soft literal with a weight.

This function declares a literal as a soft literal in the underlying MaxSAT formula. Assigning the literal to true incurs cost weight.

If the literal is already set in the formula, this overrides the previous cost the literal had.

See ipamir2022 for more details.

Parameters:

Name	Type	Description	Default
lit	int	The soft literal.	required
weight	int	The new weight for the literal.	required

add_weight

add_weight(weight)

Changes the weight for the next clause that is added literal by literal.

Parameters:

Name	Type	Description	Default
weight	int | SPECIAL_WEIGHTS	The weight for the next clause.	required

clone

clone()

Clones the current container.

Returns:

Type	Description
WClauseContainer	The cloned container.

cost

cost(assignment)

Given an assignment, return the sum of the weights for unsatisfied clauses.

Parameters:

Name	Type	Description	Default
assignment	Sequence[int]	The assignment to check.	required

Returns:

Type	Description
int	The sum of the weights of the unsatisfied clauses.

hard_clauses

hard_clauses()

Get the hard clauses in the formula.

is_feasible

is_feasible(assignment)

Checks if a given (possibly partial) assignment is feasible.

Parameters:

Name	Type	Description	Default
assignment	Sequence[int]	The assignment to check.	required

Returns:

Type	Description
bool | None	True if the assignment is feasible, False if not,
bool | None	and None if the assignment is partial and could not
bool | None	determine if it is feasible or not.

max_var

max_var()

Get the largest variable used in the container.

Returns:

Type	Description
int	The (positive) integer assigned to the largest variable.

max_weight

max_weight()

Get the highest weight from the soft clauses in the formula.

num_clauses

num_clauses()

Obtain the distribution of clauses hold by the container over weights.

This method returns the number of clauses that the container currently holds. It is implementation defined, meaning that it does not need to match the number of times that add_clause was called. For example, a simplification could be performed on the clauses, eliminating some of them.

Returns:

Type	Description
dict[int | SPECIAL_WEIGHTS, int]	The map with the distribution of clauses.

set_minimum_var

set_minimum_var(var)

Sets the maximum variable known to the container to at least this one.

This method can be used to ensure that the container knows a certain variable. If the container internally generates new variables, or if someone relies on the method to determine the next free variable, this method ensures that existing variables cannot be reused.

Parameters:

Name	Type	Description	Default
var	int	The variable to be registered to the container.	required

soft_clauses

soft_clauses()

Get the soft clauses with their weight in the formula.

total_weight

total_weight()

Get the sum of the weights of all the soft clauses in the formula.

SPECIAL_WEIGHTS

Bases: Enum