Max 2-SAT Example

Download Notebook

The Maximum 2-Satisfiability (Max2SAT) problem asks for a truth assignment that satisfies the maximum number of clauses in a 2-CNF formula. It is NP-hard.

import getpass
import os

from dotenv import load_dotenv
from luna_quantum.algorithms import SCIP

from luna_usecases.max2sat import (
    Max2satCollection,
    Max2satData,
    Max2satFormulation,
    Max2satInstance,
)

load_dotenv()
if "LUNA_API_KEY" not in os.environ:
    os.environ["LUNA_API_KEY"] = getpass.getpass("Enter your Luna API key: ")

Create Data

Generate a random Max2SAT instance with 5 variables and 10 clauses.

data = Max2satData.generate_random(size=5, n_clauses=10, seed=42)
print(data.to_string())

Max2sat Data:
  name: max2sat
  variables: 5
  clauses: 10
  Clauses list:
    0: (x_0 OR x_3)
    1: (x_3 OR x_0)
    2: (~x_2 OR ~x_4)
    3: (~x_2 OR x_3)
    4: (~x_1 OR ~x_2)
    5: (~x_2 OR x_4)
    6: (~x_4 OR ~x_1)
    7: (x_0 OR ~x_4)
    8: (x_0 OR x_3)
    9: (~x_3 OR ~x_2)

Plot Data

Visualize the bipartite variable–clause graph. Solid edges represent positive literals, dashed edges represent negated literals.

data.plot()

<Axes: title={'center': 'MAX-2SAT — 5 variables, 10 clauses'}>

Create Formulation

Set up the optimization formulation that encodes clause satisfaction.

formulation = Max2satFormulation()
print(formulation.to_string(data))

Max 2-SAT Formulation:
  Variables: 5
  Clauses: 10

Decision Variables:
  x[i] in {0,1} for i = 0, ..., 4
  x[i] = 1 if variable i is true
  Total: 5 binary variables

Objective:
  maximize sum_c (L1(c) + L2(c) - L1(c) * L2(c))
  where L(c) = x[i] if positive literal, (1 - x[i]) if negated

Constraints:
  None (unconstrained optimization)

Create Instance

Combine data and formulation into a solvable instance.

instance = Max2satInstance(data=data, formulation=formulation)
print(instance.to_string())

Data:Max2sat Data:
  name: max2sat
  variables: 5
  clauses: 10
  Clauses list:
    0: (x_0 OR x_3)
    1: (x_3 OR x_0)
    2: (~x_2 OR ~x_4)
    3: (~x_2 OR x_3)
    4: (~x_1 OR ~x_2)
    5: (~x_2 OR x_4)
    6: (~x_4 OR ~x_1)
    7: (x_0 OR ~x_4)
    8: (x_0 OR x_3)
    9: (~x_3 OR ~x_2)
Formulation:Max 2-SAT Formulation:
  Variables: 5
  Clauses: 10

Decision Variables:
  x[i] in {0,1} for i = 0, ..., 4
  x[i] = 1 if variable i is true
  Total: 5 binary variables

Objective:
  maximize sum_c (L1(c) + L2(c) - L1(c) * L2(c))
  where L(c) = x[i] if positive literal, (1 - x[i]) if negated

Constraints:
  None (unconstrained optimization)

Formulate Model

Translate the instance into a mathematical optimization model.

model = instance.formulate()
print(model)

Model: max2sat<max2sat>
Minimize
  3 * x_0 * x_3 - x_0 * x_4 + x_1 * x_2 + x_1 * x_4 - 3 * x_0 + 2 * x_2
  - 3 * x_3 + x_4 - 7
Binary
  x_0 x_1 x_2 x_3 x_4

Solve and Interpret

Solve the model with SCIP and interpret the raw result into a use-case-specific solution.

scip = SCIP()
job = scip.run(model)
sol = job.result()
uc_solution = instance.interpret(sol)
print(uc_solution.to_string())

/Users/maximilianjanetschek/PycharmProjects/luna-usecases/.venv/lib/python3.13/site-packages/rich/live.py:260:
UserWarning: install "ipywidgets" for Jupyter support
  warnings.warn('install "ipywidgets" for Jupyter support')

2026-05-29 11:35:05 INFO     Sleeping for 5.0 seconds. Waiting and checking a function in a loop.

Max2sat Solution:
  Satisfied Clauses: 10
  Valid: True
  Assignment: {0: True, 1: False, 2: False, 3: False, 4: False}
  Satisfied Indices: [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]

Plot Solution

Visualize the solution on the bipartite graph. Variable nodes are colored by their assignment (green = True, red = False), clause nodes by satisfaction status.

uc_solution.plot(data=data)

<Axes: title={'center': 'MAX-2SAT Solution — 10/10 clauses satisfied'}>

Collections

Generate a benchmark collection of random instances for batch processing.

collection = Max2satCollection.from_random(
    min_size=2,
    max_size=4,
    num_instances=2,
    seed=42,
)

print(f"Collection: {collection.name}")
print(f"Description: {collection.description}")
print(f"Total instances: {len(collection.instances)}")

Collection: Random Max2sat Set 2-4
Description: Random Max2sat instances with 2 per size
Total instances: 6