API Reference

paramita.examples module

DpllSolver

Bases: NonIncrSatSolver

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

assume

assume(lit)

Add an assumption for the next solve or propagate call.

See BALYO201645 for more details.

clone

clone()

Clones the SAT solver.

Returns:

Type	Description
NonIncrSatSolver	The cloned SAT solver.

core

core()

Retrieve the unsatisfiable core.

Returns:

Type	Description
list[int]	A vector filled with a subset of the assumptions that are jointly unsatisfiable.

failed

failed(lit)

Check if a literal belongs to the unsatisfiable core.

See BALYO201645 for more details.

Parameters:

Name	Type	Description	Default
lit	int	The literal to be checked.	required

Returns:

Type	Description
bool	true if the literal belongs to the unsatisfiable core, false otherwise.

freeze

freeze(lit)

Freeze a variable.

A frozen variable is a variable that is potentially needed in the future (for example, new assumptions). Internally, the solver can decide to perform variable elimination.

A variable can be frozen multiple times, as in Lingeling or CaDiCaL. You must call melt the same number of times to "unfreeze" a variable.

See

Parameters:

Name	Type	Description	Default
lit	int	The literal representing the variable. Only its absolute value (i.e. the variable) is considered.	required

get_phase

get_phase(lit)

Returns the default phase for a decision variable.

Parameters:

Name	Type	Description	Default
lit	int	The literal representing the decision variable. Only its absolute value (i.e. the variable) is considered.	required

Returns:

Type	Description
bool | None	True if the phase is positive, False if negative, or std::nothing if it was not set.

interrupt

interrupt()

Interrupts the resolution process.

This method instructs the solver to stop solving or propagating. Note that this is a notification, not an immediate stop, when the solver is interrupted is implementation defined.

is_fixed

is_fixed(lit)

Detect if a variable is implied at root level.

Parameters:

Name	Type	Description	Default
lit	int	The literal representing the variable. Only its absolute value (i.e. the variable) is considered.	required

Returns:

Type	Description
bool | None	True if the variable is implied by the formula, False if its negation is implied, or std::nothing if it has not yet been determined.

is_frozen

is_frozen(lit)

Checks if a variable is frozen.

Parameters:

Name	Type	Description	Default
lit	int	The literal representing the variable. Only its absolute value (i.e. the variable) is considered.	required

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.

melt

melt(lit)

Melts a variable.

Parameters:

Name	Type	Description	Default
lit	int	The literal representing the variable. Only its absolute value (i.e. the variable) is considered.	required

model

model()

Get the model (solution) after solving.

Returns:

Type	Description
list[int]	The vector where the solution will be stored. Each element of the vector is a literal that was set to true.

num_active_vars

num_active_vars()

Counts how many variables are active.

An active variable is a variable that exists in an irredundant clause (i.e. not satisfied, subsumed, or eliminated). Variable become inactive if they are eliminated or fixed at the root level.

Returns:

Type	Description
int	The number of active variables.

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.

num_conflicts

num_conflicts()

Get the number of conflicts encountered.

Returns:

Type	Description
int	The total number of conflicts found during solve.

phase

phase(lit)

Set the default phase for a decision variable during branching.

Parameters:

Name	Type	Description	Default
lit	int	The literal representing the decision variable and its phase (positive if we want the phase to be True and negative if we want it to be False).	required

propagate

propagate(assumptions)

Propagate the given assumptions.

Parameters:

Name	Type	Description	Default
assumptions	Sequence[int]	A list of literals assumed to be true.	required

Returns:

Type	Description
tuple[bool, list[int]]	A pair with a) true if propagation succeeded without a conflict, false if a conflict was found; and b) a vector with the literals propagated as a result of the assumptions. In case the propagation fails, the vector might be empty.

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

simplify

simplify(num_rounds)

Simplify the formula.

Parameters:

Name	Type	Description	Default
num_rounds	int	The number of simplification rounds to apply.	required

solve

solve(assumptions, budget)

Solve the underlying formula under the given assumptions.

If interrupted, the solver is responsible from clearing the interruption.

Parameters:

Name	Type	Description	Default
assumptions	Sequence[int]	A vector with literals that will be fixed during this solve call.	[]
budget	SolvingBudget	Solving limits for this call.	...

Returns:

Type	Description
bool | None	An option with a boolean representing the satisfiability status of the formula under the specified assumptions, or std::nullopt if it could not be determined.

unphase

unphase(lit)

Removes the default phase for a decision variable.

Parameters:

Name	Type	Description	Default
lit	int	The literal representing the decision variable. Only its absolute value (i.e. the variable) is considered.	required

val_lit

val_lit(lit)

Get the truth value for a literal.

See BALYO201645 for more details.

Parameters:

Name	Type	Description	Default
lit	int	The literal to check.	required

Returns:

Type	Description
bool | None	lit if the literal belongs to the model, -lit if its negation belongs to the model, and 0 if it is not determined.

LinearMaxSat

Bases: NonIncrMaxSatSolver

add_clause

add_clause(clause, 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

assume

assume(lit)

Add an assumption for the next solve call.

See ipamir2022 for more details.

clone

clone()

Clone the current solver.

Returns:

Type	Description
NonIncrMaxSatSolver	The cloned solver.

lower_bound

lower_bound()

Returns a lower bound on the objective value of the formula.

Returns:

Type	Description
int	The lower bound computed for the formula.

max_var

max_var()

Get the largest variable used in the container.

Returns:

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

model

model()

Get the model (solution) after solving.

The model in a MaxSAT solver will correspond to the best solution found during solving (not only from the last call).

Returns:

Type	Description
list[int]	A vector with the literals that were set to true by the last solve call.

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.

num_conflicts

num_conflicts()

The number of conflicts triggered by a solve call.

Returns:

Type	Description
int	The number of conflicts.

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

solve

solve(assumptions=[], budget=SolvingBudget())

Solve the formula under given assumptions.

The feasible solutions of the formula are assignments that satisfy all the hard clauses in the formula.

The cost of a solution is the sum of the weights of the soft clauses not satisfied by the solution.

An optimal solution is a feasible solution with minimal cost.

If interrupted, the solver is responsible from clearing the interruption.

Parameters:

Name	Type	Description	Default
assumptions	Sequence[int]	The literals manually assigned to true.	[]
budget	SolvingBudget	Budget restrictions for the solve process.	...

Returns:

Name	Type	Description
MAXSAT_ANSWER	MAXSAT_ANSWER	:UNKNOWN if no feasible solution is found and the satisfiability of hard clauses has not been determined, MAXSAT_ANSWER::SATISFIABLE if a feasible solution is found but has not been proved to be optimal, MAXSAT_ANSWER::UNSATISFIABLE if the hard clauses are proven to be unsatisfiable, and MAXSAT_ANSWER::OPTIMAL if the feasible solution is proven to be optimal (each of those cases considering the given assumptions).

val_lit

val_lit(lit)

The truth value for a literal in the best solution.

See ipamir2022 for more details.

val_objective

val_objective()

The sum of weights for satisfied soft clauses from the last feasible solution.

The objective value of a solution corresponds to the sum of all the weights for the soft clauses minus the cost of the clauses.

Returns:

Type	Description
int	The sum of the weights of the satisfied soft clauses.