Max 2-SAT API Reference

Data

Data model for Max2sat use case.

`Max2satData`

Bases: UcData

Data for the Max2sat use case.

Attributes:

Name	Type	Description
`name`	`Literal['max2sat']`	Identifier for this data type.
`clauses`	`list[Clause]`	A list containing all clauses of the formula in CNF. Each clause is a tuple of two literals. Each literal is a tuple of (variable_index, is_positive). Example: ((0, True), (1, False)) represents (x0 OR NOT x1).
`n_vars`	`int`	The number of variables in the problem.

`plot(*, ax: Axes | None = None) -> Axes`

Plot a bipartite graph of variables and clauses.

Variable nodes are placed on the left and clause nodes on the right. Solid edges indicate a positive literal; dashed edges indicate a negated literal.

Parameters:

Name	Type	Description	Default
`ax`	`Axes \| None`	Matplotlib axes to draw on. Creates a new figure if `None`.	`None`

Returns:

Type	Description
`Axes`	The axes with the plot.

`to_string() -> str`

Print the data.

Returns:

Type	Description
`str`	String representation of the data.

`from_clause_list(clauses: list[Clause], n_vars: int | None = None) -> Max2satData` `staticmethod`

Create Max2satData from a list of clauses.

Parameters:

Name	Type	Description	Default
`clauses`	`list[Clause]`	A list of clauses. Each clause is a tuple of two literals, where each literal is a tuple of (variable_index, is_positive). Example: `[((0, True), (1, False)), ((1, True), (2, True))]`.	required
`n_vars`	`int \| None`	The number of variables. If None, inferred as one more than the highest variable index appearing in the clauses.	`None`

Returns:

Type	Description
`Max2satData`	A Max2sat data instance.

Raises:

Type	Description
`ValueError`	If `clauses` is empty and `n_vars` is not provided, or if `n_vars` is less than the number of variables in the clauses.

Examples:

>>> clauses = [((0, True), (1, False)), ((1, True), (2, True))]
>>> data = Max2satData.from_clause_list(clauses)

`generate_random(size: int = 10, n_clauses: int | None = None, seed: int | None = None) -> Max2satData` `staticmethod`

Generate a random instance.

Parameters:

Name	Type	Description	Default
`size`	`int`	Number of variables, by default 10.	`10`
`n_clauses`	`int \| None`	Number of clauses. If None, defaults to 2 * size.	`None`
`seed`	`int \| None`	Random seed for reproducibility, by default None.	`None`

Returns:

Type	Description
`Max2satData`	A randomly generated data instance.

Examples:

>>> data = Max2satData.generate_random(size=20, n_clauses=40, seed=42)

Formulation

Formulation for Max2sat use case.

`Max2satFormulation`

Bases: UcFormulation[Max2satData, Max2satSolution]

Constraint-based formulation for Max2sat.

This formulation creates a QUBO model where the objective is to maximize the number of satisfied clauses. It uses LunaModel's constraint system rather than manual QUBO penalty terms.

Mathematical Formulation

Decision Variables:
    # Example: x_i ∈ {0,1} for each item i

Objective:
    # Example: maximize Σ_i (value_i * x_i)

Constraints:
    # Example: Σ_i (weight_i * x_i) ≤ capacity

`to_string(data: Max2satData) -> str` `staticmethod`

Print the formulation.

Parameters:

Name	Type	Description	Default
`data`	`Max2satData`	The problem data.	required

Returns:

Type	Description
`str`	String representation of the formulation.

`formulate(data: Max2satData) -> Model` `staticmethod`

Formulate using constraint-based approach.

IMPORTANT: Use model.add_constraint() for constraints. Do NOT use manual QUBO penalty terms (no A, B parameters).

Parameters:

Name	Type	Description	Default
`data`	`Max2satData`	The problem data.	required

Returns:

Type	Description
`Model`	A LunaModel ready to be solved.

Examples:

Basic structure:

>>> model = Model(name="problem_name")
>>> # Create variables
>>> with model.environment:
...     x = {i: Variable(f"x_{i}", vtype=Vtype.BINARY) for i in range(n)}
>>> # Set objective (negate if maximizing)
>>> objective = -quicksum(value[i] * x[i] for i in range(n))
>>> # Add constraints (NOT penalty terms!)
>>> model.add_constraint(
...     quicksum(weight[i] * x[i] for i in range(n)) <= capacity,
...     name="capacity_constraint",
... )
>>> model.set_objective(objective)
>>> model.set_sense(Sense.MIN)
>>> return model

`interpret(solution: Solution, data: Max2satData) -> Max2satSolution` `staticmethod`

Extract solution from quantum result.

Parameters:

Name	Type	Description	Default
`solution`	`Solution`	The quantum solution.	required
`data`	`Max2satData`	The problem data.	required

Returns:

Type	Description
`Max2satSolution`	Structured solution with metrics.

Solution

Solution model for Max2sat use case.

`Max2satSolution`

Bases: UcSolution

Solution for the Max2sat use case.

Attributes:

Name	Type	Description
`name`	`Literal['max2sat']`	Identifier for this solution type.
`assignment`	`dict[int, bool]`	A dictionary mapping variable indices to their boolean assignment. Example: {0: True, 1: False} means x_0 is True, x_1 is False.
`num_satisfied`	`int`	The number of clauses satisfied by this assignment.
`satisfied_clause_indices`	`list[int]`	Indices of the clauses that are satisfied by the assignment.
`is_valid`	`bool`	Whether the solution is valid (all variables assigned).

`plot(data: Max2satData | None = None, *, ax: Axes | None = None) -> Axes`

Plot the MAX-2SAT solution.

When data is provided, draws a bipartite variable-clause graph with clause nodes colored green (satisfied) or red (unsatisfied). Without data, displays a single horizontal bar showing the number of satisfied clauses.

Parameters:

Name	Type	Description	Default
`data`	`Max2satData \| None`	Problem data. When provided, the full bipartite graph is drawn with satisfaction coloring.	`None`
`ax`	`Axes \| None`	Matplotlib axes to draw on. Creates a new figure if `None`.	`None`

Returns:

Type	Description
`Axes`	The axes with the plot.

`to_string() -> str`

Print the solution.

Returns:

Type	Description
`str`	String representation of the solution.

Instance

Instance model for Max2sat use case.

`Max2satInstance`

Bases: UcInstance[Max2satData, Max2satFormulation, Max2satSolution]

Instance combining data and formulation for Max2sat.

Collection

Collection of Max2sat instances.

`Max2satCollection`

Bases: UcInstanceCollection[Max2satInstance]

Collection of Max2sat instances.

This collection provides methods to generate benchmark instances with various characteristics for testing and evaluation.

`from_random(min_size: int | None = None, max_size: int | None = None, num_instances: int = 1, seed: int | None = None, *, sizes: Sequence[int] | None = None) -> Max2satCollection` `classmethod`

Generate random instances.

Parameters:

Name	Type	Description	Default
`min_size`	`int \| None`	Minimum problem size.	`None`
`max_size`	`int \| None`	Maximum problem size.	`None`
`num_instances`	`int`	Number of instances per size, by default 1.	`1`
`seed`	`int \| None`	Random seed for reproducibility, by default None.	`None`
`sizes`	`Sequence[int] \| None`	Explicit sizes to generate, e.g. `[10, 50, 100]`, instead of a range. Mutually exclusive with `min_size`/`max_size`, by default None.	`None`

Returns:

Type	Description
`Max2satCollection`	Collection containing generated instances.

Examples:

>>> collection = Max2satCollection.from_random(
...     min_size=5,
...     max_size=10,
...     num_instances=3,
...     seed=42,
... )

`filter_infeasible(max_runtime: float = 3600, *, quiet: bool = True) -> list[bool]`

Drop the instances of this collection that have no feasible solution.

Every instance is formulated and handed to SCIP, which stops as soon as it finds the first feasible solution. An instance is removed from the collection when SCIP proves the model infeasible, when no solution turns up within max_runtime, or when formulating it fails altogether. This keeps randomly generated instances from breaking a downstream pipeline.

Parameters:

Name	Type	Description	Default
`max_runtime`	`float`	SCIP time limit per instance in seconds. Must be positive. Defaults to 3600 seconds.	`3600`
`quiet`	`bool`	Suppress the SCIP solver output.	`True`

Returns:

Type	Description
`list[bool]`	Feasibility mask over the instances as they were before filtering, in that order: `True` where the instance was kept, `False` where it was removed.

Raises:

Type	Description
`ValueError`	If `max_runtime` is not positive.

Max 2-SAT API Reference

Data

Max2satData

plot(*, ax: Axes | None = None) -> Axes

to_string() -> str

from_clause_list(clauses: list[Clause], n_vars: int | None = None) -> Max2satData staticmethod

generate_random(size: int = 10, n_clauses: int | None = None, seed: int | None = None) -> Max2satData staticmethod

Formulation

Max2satFormulation

to_string(data: Max2satData) -> str staticmethod

formulate(data: Max2satData) -> Model staticmethod

interpret(solution: Solution, data: Max2satData) -> Max2satSolution staticmethod

Solution

Max2satSolution

plot(data: Max2satData | None = None, *, ax: Axes | None = None) -> Axes

to_string() -> str

Instance

Max2satInstance

Collection

Max2satCollection

from_random(min_size: int | None = None, max_size: int | None = None, num_instances: int = 1, seed: int | None = None, *, sizes: Sequence[int] | None = None) -> Max2satCollection classmethod

filter_infeasible(max_runtime: float = 3600, *, quiet: bool = True) -> list[bool]

`Max2satData`

`plot(*, ax: Axes | None = None) -> Axes`

`to_string() -> str`

`from_clause_list(clauses: list[Clause], n_vars: int | None = None) -> Max2satData` `staticmethod`

`generate_random(size: int = 10, n_clauses: int | None = None, seed: int | None = None) -> Max2satData` `staticmethod`

`Max2satFormulation`

`to_string(data: Max2satData) -> str` `staticmethod`

`formulate(data: Max2satData) -> Model` `staticmethod`

`interpret(solution: Solution, data: Max2satData) -> Max2satSolution` `staticmethod`

`Max2satSolution`

`plot(data: Max2satData | None = None, *, ax: Axes | None = None) -> Axes`

`to_string() -> str`

`Max2satInstance`

`Max2satCollection`

`from_random(min_size: int | None = None, max_size: int | None = None, num_instances: int = 1, seed: int | None = None, *, sizes: Sequence[int] | None = None) -> Max2satCollection` `classmethod`

`filter_infeasible(max_runtime: float = 3600, *, quiet: bool = True) -> list[bool]`