API Reference

paramita.solvers module

SolvingBudget

A budget for the underlying solver.

The budget allows to set a limit to the solvers based on different limits. Currently the supported limits are:

• num_conflicts: Number of conflicts
• num_propagations: Number of propagations
• cpu_time_seconds: CPU Time in seconds

NonIncrSatSolver

Bases: ClauseContainer

A SAT solver.

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.

SatSolver

Bases: NonIncrSatSolver

An incremental SAT Solver.

Incremental solvers allow to modify the formula and call solve as many times as needed. After modifying the formula (by adding new clauses), solve with the same parameters (i.e. assumptions, budgets...) can return different values.

add_observed_var

add_observed_var(var)

Marks a variable as observed by the external propagator.

The solver notifies the propagator about assignments involving observed variables.

Parameters:

Name	Type	Description	Default
var	int	The variable to observe.	required

assume

assume(lit)

Add an assumption for the next solve or propagate call.

See BALYO201645 for more details.

clone

clone()

Clones the incremental SAT solver.

Returns:

Type	Description
SatSolver	The cloned incremental SAT solver.

connect_external_propagator

connect_external_propagator(propagator)

Connects an external to the solver.

The propagator receives notifications about the solver state and may perform external propagation, suggest branching decisions, reject candidate models, and add external clauses.

Only one propagator can be connected at a time. Connecting a new propagator replaces any previously connected propagator.

Parameters:

Name	Type	Description	Default
propagator	Propagator	The propagator to connect.	required

connect_learner

connect_learner(learner)

Connects a to the solver.

The learner receives learnt clauses generated during solving according to its is_relevant() criterion.

Only one learner can be connected at a time. Connecting a new learner replaces any previously connected learner.

Parameters:

Name	Type	Description	Default
learner	Learner	The learner to connect.	required

core

core()

Retrieve the unsatisfiable core.

Returns:

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

disconnect_external_propagator

disconnect_external_propagator()

Disconnects the currently connected external propagator.

After this call, the solver no longer issues notifications or callbacks to the propagator.

disconnect_learner

disconnect_learner()

Disconnects the currently connected learner.

After this call, learnt clauses are no longer reported.

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.

force_backtrack

force_backtrack(new_level)

Forces the solver to backtrack.

Parameters:

Name	Type	Description	Default
new_level	int	The decision level to backtrack to.	required

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_decision

is_decision(lit)

Checks whether a literal is assigned as a decision.

Parameters:

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

Returns:

Type	Description
bool	true if the literal is a decision assignment, false otherwise.

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

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_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.

remove_observed_var

remove_observed_var(var)

Stops observing a variable.

After this call, assignments to the variable are no longer reported to the external propagator.

Parameters:

Name	Type	Description	Default
var	int	The variable to stop observing.	required

reset_observed_vars

reset_observed_vars()

Removes all observed variables.

After this call, no variable is observed until new ones are added using .

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.

NonIncrMaxSatSolver

Bases: WClauseContainer

A MaxSAT solver.

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

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=...)

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.

MaxSatSolver

Bases: NonIncrMaxSatSolver

An incremental MaxSAT solver.

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
MaxSatSolver	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.

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_conflicts

num_conflicts()

The number of conflicts triggered by a solve call.

Returns:

Type	Description
int	The number of conflicts.

solve

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

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.

MAXSAT_ANSWER

Bases: Enum

Represents the answer for a MaxSAT solve call.

NotSolvedException

Bases: Exception

UnsatisfiableException

Bases: Exception

Propagator

Bases: Plugin

Interface for implementing external propagation.

A extends the behavior of a SAT solver by maintaining its own state alongside the solver state. The solver notifies the propagator of assignments and backtracking events, and the propagator may in turn:

• Propagate additional literals.
• Provide explanations (reason clauses) for propagated literals.
• Suggest branching decisions.
• Reject candidate models.
• Add external clauses to the solver.

check_found_model

check_found_model(model)

Checks whether a candidate model is acceptable.

The solver calls this method when it has found a model.

Parameters:

Name	Type	Description	Default
model	Sequence[int]	The candidate model.	required

Returns:

Type	Description
bool	true if the model is accepted, false otherwise.

decide

decide()

Suggests the next branching literal.

Returning 0 indicates that the propagator does not provide a decision and the solver should use its own branching heuristic.

Returns:

Type	Description
int	The next decision literal, or 0 if none is suggested.

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_external_clause

get_external_clause()

Returns an external clause to be added to the solver.

This method is called only if returns true.

Returns:

Type	Description
list[int]	The external clause.

get_parameter_space

get_parameter_space()

Get the parameter space for this class.

Returns:

Type	Description
ParameterSpace	The parameter space.

get_reason_clause

get_reason_clause(propagated_lit)

Returns the reason clause for a propagated literal.

The returned clause must justify the propagation of propagated_lit.

Parameters:

Name	Type	Description	Default
propagated_lit	int	The propagated literal.	required

Returns:

Type	Description
list[int]	The reason clause.

has_external_clause

has_external_clause()

Indicates whether the propagator has an external clause to add.

Returns:

Type	Description
bool	true if an external clause is available, false otherwise.

on_assignment

on_assignment(lits)

Notifies the propagator of newly assigned literals.

The propagator should update its internal state to reflect the assignments.

Parameters:

Name	Type	Description	Default
lits	Sequence[int]	The literals assigned since the previous notification.	required

on_backtrack

on_backtrack(new_level)

Notifies the propagator that the solver has backtracked.

The propagator should restore its internal state to match the given decision level.

Parameters:

Name	Type	Description	Default
new_level	int	The decision level after backtracking.	required

on_new_decision_level

on_new_decision_level()

Notifies the propagator about a new decision level.

propagate

propagate()

Performs external propagation.

Returns:

Type	Description
list[int]	A list of literals that should be propagated by the solver.

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

Learner

Bases: Plugin

Interface for components that consume learnt clauses.

A can be attached to a SAT solver to receive learnt clauses generated during the solving process. Implementations can use this information for tasks such as collecting statistics, learning new models, or building heuristics.

Before a learnt clause is reported, the solver calls to determine whether clauses of a given size should be forwarded to the learner.

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.

is_relevant

is_relevant(size)

Determines whether a learnt clause is relevant based on its size.

The solver calls this method before forwarding a learnt clause. If it returns true, the clause is passed to . Otherwise, the clause is ignored.

Parameters:

Name	Type	Description	Default
size	int	The number of literals in the learnt clause.	required

Returns:

Type	Description
bool	true if learnt clauses of the given size should be reported; false otherwise.

learnt

learnt(clause)

Reports a learnt clause.

This method is called for every learnt clause considered relevant by .

Parameters:

Name	Type	Description	Default
clause	Sequence[int]	The learnt clause represented as a vector of literals.	required

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