Max 3-SAT Example

Download Notebook

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

import getpass
import os

from dotenv import load_dotenv
from luna_quantum.algorithms import SCIP

from luna_usecases.max3sat import (
    Max3satCollection,
    Max3satData,
    Max3satFormulation,
    Max3satInstance,
)

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 Max3SAT instance with 5 variables and 10 clauses.

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

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

Plot Data

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

data.plot()

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

Create Formulation

Set up the optimization formulation that encodes clause satisfaction.

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

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

Decision Variables:
  v[i] in {0,1} for i = 0, ..., 4  (truth value of variable i)
  s[c] in {0,1} for c = 0, ..., 9  (whether clause c is satisfied)
  Total: 15 binary variables

Objective:
  maximize sum_c s[c]

Constraints:
  1. Clause satisfaction (10 constraints):
     s[c] <= expr(l1) + expr(l2) + expr(l3)  for all c = 0, ..., 9
     where expr(i, True) = v[i], expr(i, False) = 1 - v[i]

Create Instance

Combine data and formulation into a solvable instance.

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

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

Decision Variables:
  v[i] in {0,1} for i = 0, ..., 4  (truth value of variable i)
  s[c] in {0,1} for c = 0, ..., 9  (whether clause c is satisfied)
  Total: 15 binary variables

Objective:
  maximize sum_c s[c]

Constraints:
  1. Clause satisfaction (10 constraints):
     s[c] <= expr(l1) + expr(l2) + expr(l3)  for all c = 0, ..., 9
     where expr(i, True) = v[i], expr(i, False) = 1 - v[i]

Formulate Model

Translate the instance into a mathematical optimization model.

model = instance.formulate()
print(model)

Model: max3sat<max3sat>
Maximize
  s_0 + s_1 + s_2 + s_3 + s_4 + s_5 + s_6 + s_7 + s_8 + s_9
Subject To
  clause_0: -v_0 + v_3 + v_4 + s_0 <= 2
  clause_1: v_0 + v_2 + v_3 + s_1 <= 3
  clause_2: v_0 - v_1 - v_4 + s_2 <= 1
  clause_3: -v_2 - v_3 - v_4 + s_3 <= 0
  clause_4: v_0 - v_2 + v_4 + s_4 <= 2
  clause_5: -v_0 + v_3 + v_4 + s_5 <= 2
  clause_6: -v_2 - v_3 - v_4 + s_6 <= 0
  clause_7: -v_0 + v_1 + v_3 + s_7 <= 2
  clause_8: v_1 - v_3 - v_4 + s_8 <= 1
  clause_9: v_0 + v_1 - v_3 + s_9 <= 2
Binary
  v_0 v_1 v_2 v_3 v_4 s_0 s_1 s_2 s_3 s_4 s_5 s_6 s_7 s_8 s_9

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:07 INFO     Sleeping for 5.0 seconds. Waiting and checking a function in a loop.

Max3sat Solution:
  Satisfied Clauses: 10
  Valid: True
  Assignment: {0: False, 1: False, 2: False, 3: True, 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-3SAT Solution — 10/10 clauses satisfied'}>

Collections

Generate a benchmark collection of random instances for batch processing.

collection = Max3satCollection.from_random(
    min_size=3,
    max_size=5,
    num_instances=2,
    seed=42,
)

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

Collection: Random Max3sat Set 3-5
Description: Random Max3sat instances with 2 per size
Total instances: 6