Max 2-SAT API Reference

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.

Print the data.

Returns:

• str –

  String representation of the data.

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:

• Max2satData –

  A Max2sat data instance.

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

• Max2satData –

  A randomly generated data instance.

Examples:

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

Print the formulation.

Parameters:

• data (Max2satData) –

  The problem data.

Returns:

• str –

  String representation of the formulation.

Formulate using constraint-based approach.

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

Parameters:

• data (Max2satData) –

  The problem data.

Returns:

• 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

Extract solution from quantum result.

Parameters:

• solution (Solution) –

  The quantum solution.

• data (Max2satData) –

  The problem data.

Returns:

• Max2satSolution –

  Structured solution with metrics.

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.

Print the solution.

Returns:

• str –

  String representation of the solution.

Generate random instances.

Parameters:

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

  Minimum problem size.

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

  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.

• sizes (Sequence[int] | None, default: None ) –

  Explicit sizes to generate, e.g. [10, 50, 100], instead of a range. Mutually exclusive with min_size/max_size, by default None.

Returns:

• Max2satCollection –

  Collection containing generated instances.

Examples:

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

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:

• max_runtime (float, default: 3600 ) –

  SCIP time limit per instance in seconds. Must be positive. Defaults to 3600 seconds.

• quiet (bool, default: True ) –

  Suppress the SCIP solver output.

Returns:

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

• ValueError –

  If max_runtime is not positive.