API Reference

paramita.decoders module

CnfToPbDecoder

Bases: Plugin

A decoder from CNF to Pseudo-Boolean (PB) constraints.

A decoder analyzes a CNF formula and reconstructs one or more PB constraints that are semantically equivalent to a subset of the clauses.

The decoder operates on a and uses a set of target literals from where constraints will be detected.

decode

decode(container, target_lits)

Decode PB constraints from a CNF formula.

An implementation analyzes the clauses stored in the given and reconstructs any PB constraints it recognizes. The target_lits parameter is used to restrict the search to constraints involving specific literals.

Parameters:

Name	Type	Description	Default
container	ClauseContainer	The containing the CNF formula to analyze.	required
target_lits	Sequence[int]	The literals of interest for the decoding process.	required

Returns:

Type	Description
list[PbConstraint]	A vector containing the decoded PB constraints.

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.

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