Produce a satisfying assignment for a TfP-generated DIMACS CNF instance: 30 variables, 130 clauses. The sandbox check is followed by a human reviewer confirming the witness — the Stage 7B review dogfood.
A result is verified when the submitted assignment file, parsed as SAT-competition v-line format, assigns every variable of the bound CNF instance and satisfies all of its clauses. Assignments mentioning variables outside the instance are rejected. This establishes that the instance is satisfiable and that this assignment witnesses it. It does not establish that the assignment is unique or minimal. A campaign reviewer then confirms the submission is a genuine witness rather than a bulk dump.