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 Luna Model'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 Luna Model 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, max_size: int, num_instances: int = 1, seed: int | None = None) -> Max2satCollection` `classmethod`

Generate random instances.

Parameters:

Name	Type	Description	Default
`min_size`	`int`	Minimum problem size.	required
`max_size`	`int`	Maximum problem size.	required
`num_instances`	`int`	Number of instances per size, by default 1.	`1`
`seed`	`int \| None`	Random seed for reproducibility, 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,
... )

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, max_size: int, num_instances: int = 1, seed: int | None = None) -> Max2satCollection classmethod

`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, max_size: int, num_instances: int = 1, seed: int | None = None) -> Max2satCollection` `classmethod`