Skip to content

Max 2-SAT API Reference

Data

Data model for Max2sat use case.

Max2satData

Bases: UcData

Data for the Max2sat use case.

Attributes:

  • 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:

  • ax (Axes | None, default: None ) –

    Matplotlib axes to draw on. Creates a new figure if None.

Returns:

  • Axes –

    The axes with the plot.

to_string() -> str

Print the data.

Returns:

  • 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:

  • 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))].

  • n_vars (int | None, default: None ) –

    The number of variables. If None, inferred as one more than the highest variable index appearing in the clauses.

Returns:

Raises:

  • 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:

  • size (int, default: 10 ) –

    Number of variables, by default 10.

  • n_clauses (int | None, default: None ) –

    Number of clauses. If None, defaults to 2 * size.

  • seed (int | None, default: None ) –

    Random seed for reproducibility, by default None.

Returns:

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:

Returns:

  • 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:

Returns:

  • 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:

  • solution (Solution) –

    The quantum solution.

  • data (Max2satData) –

    The problem data.

Returns:

Solution

Solution model for Max2sat use case.

Max2satSolution

Bases: UcSolution

Solution for the Max2sat use case.

Attributes:

  • 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:

  • data (Max2satData | None, default: None ) –

    Problem data. When provided, the full bipartite graph is drawn with satisfaction coloring.

  • ax (Axes | None, default: None ) –

    Matplotlib axes to draw on. Creates a new figure if None.

Returns:

  • Axes –

    The axes with the plot.

to_string() -> str

Print the solution.

Returns:

  • 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:

  • min_size (int) –

    Minimum problem size.

  • max_size (int) –

    Maximum problem size.

  • num_instances (int, default: 1 ) –

    Number of instances per size, by default 1.

  • seed (int | None, default: None ) –

    Random seed for reproducibility, by default None.

Returns:

Examples:

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