Max-3-SAT

Source: examples/max3sat/README.md

Given M clauses of 3 positive literals over N binary variables, find the assignment that satisfies the maximum number of clauses.

QUBO formulation

• Input: N binary variables, M clauses of 3 positive literals
• Model: N binary variables. x_v in {0, 1}.
• Objective: minimise sum over clauses of P*(1-x_i)(1-x_j)(1-x_k)

A clause (i,j,k) is violated when all three variables are 0. Expanding the product (dropping the constant term):

P*(-x_i - x_j - x_k + x_i*x_j + x_i*x_k + x_j*x_k - x_i*x_j*x_k)

The cubic term -P*x_i*x_j*x_k is degree-reduced via REDUCE(i, j) -> w, introducing one auxiliary variable w per clause with Rosenberg enforcement P_AUX*(x_i*x_j - 2*x_i*w - 2*x_j*w + 3*w). The cubic term becomes the quadratic term -P*w*x_k.

DSL methods used

• model.reduce(var_a, var_b, p_aux) – HOBO degree reduction; returns a RegLoad holding the auxiliary variable index for chaining into quadratic terms

Pipeline overview

1. CP (xqcp) – generate random 3-literal clauses, declare binary variables, and degree-reduce the cubic violation terms via REDUCE.
2. Assemble – .xqasm text to bytecode via xquad.asm
3. Encode – run encoder on chosen XQVM to produce the XQMX model
4. Sample – solver runs SA/QPU/GPU over the model
5. Verify – verifier checks the sample is binary and that each Rosenberg REDUCE auxiliary equals the product it stands for, then computes energy
6. Decode – decoder extracts the variable assignment

Usage

uv run python examples/max3sat/runner.py --seed 42
uv run python examples/max3sat/runner.py --n 8 --m 10 --interpreter rust

Choosing a solver

Solver selection and install extras are the same for every example: see Using the Examples and Solving Overview. The default is dwave-cpu, and a non-default solver will not reproduce the canonical result.

Canonical output

example-smoke validates both interpreters produce valid == 1 with --seed 42 --solver dwave-cpu. The smoke test is invariant-based – it checks validity, not exact output.