MAX-SAT marathon · 1000 variables

you send

1000 characters of 0 and 1.

we check

Counts the clauses your assignment breaks.

score

broken clauses, lower wins.

baseline

64 · plain WalkSAT, 5.1M flips, 20 s on one CPU core

how hard

every clause you fix is real progress

{
  "id": "maxsat-1000",
  "kind": "max-3-sat",
  "seed": "polytime/arena/v1/maxsat-1000",
  "n": 1000,
  "m": 5000,
  "dimacsUrl": "/api/arena/maxsat-1000/instance?format=cnf",
  "rule": "Score = number of unsatisfied clauses. Lower is better.",
  "answer": {
    "bits": "1000 chars of 0/1, variable 1 first (or a DIMACS v-line)"
  }
}