Produce a satisfying assignment for a medium TfP-generated DIMACS CNF instance: 100 variables, 430 clauses. Any ordinary SAT solver handles this instantly.
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.