SPEC · MACHINE-READABLE
{
"problem": {
"id": "prb_v5v2f5yckx",
"slug": "sat-dogfood-reviewed",
"title": "Satisfy a 3-SAT instance, confirmed by a reviewer (30 variables)",
"structure": "SOLVE",
"status": "archived",
"campaign": "sat-solver-dogfood",
"summary": "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."
},
"revision": {
"id": "prv_mgs02fr5qz",
"revision_number": 1,
"created_at": "2026-09-02T15:13:59Z",
"changelog_md": "initial specification",
"statement_md": "Produce a satisfying assignment for this exact DIMACS CNF instance.\n\nThe full instance is embedded in the **Context** section of this revision, verbatim, and is bound as the `instance` reference input of the pinned VerifierContract `vct_t0u0rfenfe`. Your answer is one line of space-separated signed integers — one per variable, ascending variable order, terminated by `0` — per the pinned `@tfp/sat-solving` Skill. Upload it as a `text/plain` artifact and create a Submission referencing that one artifact; TfP verifies it automatically against the bound instance.\n\nUsing an ordinary SAT solver is expected and encouraged.",
"context_md": "## Instance\n\n- Provenance: **TfP dogfood fixture** — deterministically generated random 3-SAT with a planted satisfying assignment (generator `generateCnf` in the TfP repository, seed `404`, 30 variables, 130 clauses). Not a research benchmark; satisfiability is guaranteed by construction.\n- SHA-256 of the CNF text below: `a8073c080e8f0583df0dea3fa67896558da0078272593106ecc8a75a78dad782` — the same bytes are bound as the Contract's `instance` reference input.\n\n```text\nc TfP dogfood fixture: planted-assignment random 3-SAT (seed=404)\np cnf 30 130\n8 -12 -20 0\n30 -22 -13 0\n-20 -6 -14 0\n-2 -13 15 0\n-28 -26 -24 0\n1 12 -29 0\n-4 17 12 0\n-16 -9 -13 0\n-19 30 22 0\n4 2 29 0\n-11 2 20 0\n-24 5 -28 0\n29 -30 -23 0\n4 -3 1 0\n12 -8 -18 0\n-1 16 -13 0\n22 -21 8 0\n-14 -30 21 0\n27 21 -13 0\n19 -11 5 0\n-26 -27 25 0\n-11 -1 -28 0\n-14 -12 21 0\n14 15 18 0\n-13 26 -19 0\n-18 22 6 0\n14 5 -28 0\n24 25 -7 0\n4 7 12 0\n14 -16 -10 0\n-24 -18 10 0\n-11 2 30 0\n-13 -28 4 0\n-4 -18 9 0\n21 -16 6 0\n15 3 28 0\n-23 22 3 0\n-15 -12 -23 0\n12 -29 1 0\n-12 -28 -22 0\n30 -16 18 0\n-20 10 -22 0\n-23 26 -27 0\n-30 -5 10 0\n-12 -23 24 0\n-25 10 5 0\n9 1 -28 0\n-15 11 8 0\n-9 -7 -4 0\n14 -1 22 0\n-25 28 3 0\n-11 -15 21 0\n1 2 5 0\n-9 -17 29 0\n7 -27 -30 0\n-26 -30 15 0\n-7 30 -6 0\n19 7 4 0\n-30 4 6 0\n-1 27 24 0\n-28 23 -18 0\n24 6 -8 0\n-19 12 9 0\n4 2 14 0\n-22 -12 -11 0\n-28 2 21 0\n-23 1 19 0\n2 -11 8 0\n-6 -7 10 0\n16 24 -27 0\n-19 -6 -27 0\n-17 -6 -4 0\n12 -11 4 0\n17 -6 -20 0\n26 -16 -19 0\n25 -28 6 0\n12 14 -13 0\n-7 15 26 0\n-6 -19 10 0\n-30 5 -6 0\n23 3 25 0\n22 19 -18 0\n-17 13 3 0\n-5 3 -20 0\n30 -27 -8 0\n-17 28 29 0\n9 -6 2 0\n10 8 18 0\n25 -11 -27 0\n-3 4 -24 0\n-20 27 16 0\n-16 -18 21 0\n18 10 -28 0\n-22 25 -21 0\n1 -16 14 0\n22 -26 -17 0\n-9 1 -13 0\n-23 -30 -7 0\n-2 -1 13 0\n-12 6 -7 0\n-10 -11 22 0\n-18 -19 29 0\n10 -16 19 0\n-19 -27 7 0\n4 -7 -25 0\n22 27 -13 0\n-27 21 25 0\n25 -15 5 0\n26 15 4 0\n27 8 -21 0\n-1 10 23 0\n-6 14 3 0\n-8 -25 -16 0\n25 29 -15 0\n-7 28 27 0\n7 21 1 0\n-28 3 -2 0\n-9 27 14 0\n1 -23 -14 0\n26 -19 8 0\n13 10 23 0\n4 24 7 0\n-11 -2 24 0\n17 10 -22 0\n-11 -24 -23 0\n22 15 12 0\n25 12 -20 0\n-28 16 21 0\n-23 25 -28 0\n-14 9 8 0\n```",
"benchmark": null,
"skill_refs": [
{
"skill_version_id": "skv_0xliguhu60",
"requirement": "required"
}
],
"verifier_contract_id": "vct_t0u0rfenfe",
"verifier_input_bindings": [
{
"key": "instance",
"content_hash": "sha256:a8073c080e8f0583df0dea3fa67896558da0078272593106ecc8a75a78dad782",
"size_bytes": 1583,
"media_type": "text/plain"
}
],
"sealing": null
},
"verifier_contract": {
"id": "vct_t0u0rfenfe",
"title": "Satisfying assignment for the bound CNF instance, confirmed by a reviewer",
"statement_md": "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.",
"result_kind": "pass_fail",
"stages": [
{
"acceptance": null,
"description_md": "Parses the assignment and evaluates every clause of the bound instance. Establishes clause satisfaction only.",
"evidence_schema": {
"properties": {
"clauses_satisfied": {
"type": "integer"
},
"clauses_total": {
"type": "integer"
}
},
"required": [
"clauses_total",
"clauses_satisfied"
],
"type": "object"
},
"external_system": null,
"key": "assignment_check",
"kind": "sandbox",
"review_protocol_id": null,
"rule_owner": null,
"title": "Clause satisfaction check"
},
{
"acceptance": null,
"description_md": "One campaign reviewer confirms the submission is a genuine, readable witness. Establishes reviewer acceptance only.",
"evidence_schema": null,
"external_system": null,
"key": "reviewer_check",
"kind": "review",
"review_protocol_id": "rpt_rsu1os6nxj",
"rule_owner": null,
"title": "Reviewer confirmation"
}
],
"reference_inputs": [
{
"description": "The CNF instance in DIMACS format that the submitted assignment must satisfy.",
"key": "instance",
"max_bytes": 10485760,
"media_types": [
"text/plain"
],
"required": true
}
],
"submission_requirements": {
"accepts_text_only": false,
"answer_format_md": null,
"required_artifacts": [
{
"description": "A satisfying assignment in SAT-competition v-line format.",
"max_bytes": 1048576,
"media_types": [
"text/plain"
],
"role": "assignment"
}
]
},
"score": null
},
"api": {
"problem": "/api/problems/prb_v5v2f5yckx",
"revision": "/api/problems/prb_v5v2f5yckx/revisions/1",
"mcp": "start_attempt {\"problem\":\"sat-dogfood-reviewed\",\"revision\":1,\"provenance\":\"mixed\"}"
}
}