Satisfy a small 3-SAT instance (20 variables)

{
  "problem": {
    "id": "prb_xdh2822hya",
    "slug": "sat-dogfood-small",
    "title": "Satisfy a small 3-SAT instance (20 variables)",
    "structure": "SOLVE",
    "status": "archived",
    "campaign": "sat-solver-dogfood",
    "summary": "Produce a satisfying assignment for a small TfP-generated DIMACS CNF instance: 20 variables, 91 clauses. Solvable by hand or with any SAT solver."
  },
  "revision": {
    "id": "prv_n5cfi8w9rh",
    "revision_number": 1,
    "created_at": "2026-09-02T06:59:47Z",
    "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_wacbq9qe4y`. 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 `101`, 20 variables, 91 clauses). Not a research benchmark; satisfiability is guaranteed by construction.\n- SHA-256 of the CNF text below: `eef24648920b3ca871342d0b1554341c350de9bf3ec1230aa0b4a578a6ced3cf` — 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=101)\np cnf 20 91\n16 6 -2 0\n9 -18 15 0\n-3 11 1 0\n20 9 -3 0\n10 19 -3 0\n-8 16 -3 0\n18 -8 -5 0\n2 -3 -16 0\n-5 -13 -14 0\n17 13 -12 0\n-11 20 17 0\n-20 2 -8 0\n-3 18 12 0\n6 11 2 0\n11 10 7 0\n17 18 15 0\n-7 -6 20 0\n-14 20 -15 0\n18 -11 8 0\n-9 10 1 0\n-6 5 14 0\n2 9 14 0\n-12 17 -8 0\n-1 20 -17 0\n-4 13 -18 0\n2 10 -6 0\n-12 11 -2 0\n11 -4 6 0\n9 -6 11 0\n13 1 -6 0\n10 -14 -3 0\n16 -7 -6 0\n5 16 -7 0\n8 9 -2 0\n-14 6 -13 0\n-8 17 -13 0\n9 -10 -12 0\n13 -17 -20 0\n2 11 -3 0\n-7 10 -12 0\n12 11 -4 0\n20 -11 5 0\n-8 -7 15 0\n5 1 -2 0\n4 9 -16 0\n10 20 12 0\n-4 13 -14 0\n-8 3 6 0\n1 -13 20 0\n3 -5 18 0\n-6 11 1 0\n-7 -1 -18 0\n-7 -2 -9 0\n-16 -8 3 0\n10 -11 2 0\n11 14 16 0\n-7 -12 5 0\n20 -7 -19 0\n11 -8 9 0\n-4 11 -19 0\n-5 6 9 0\n-13 1 4 0\n6 -3 2 0\n15 -2 10 0\n-19 -16 -6 0\n18 2 7 0\n2 -5 -3 0\n17 -2 13 0\n-14 -17 -6 0\n11 13 1 0\n4 -14 18 0\n-3 -15 1 0\n19 8 -6 0\n10 -4 -8 0\n-17 -10 1 0\n-14 -7 -17 0\n-6 1 5 0\n-7 20 -14 0\n16 -4 -8 0\n-6 -5 7 0\n12 8 13 0\n16 1 -14 0\n9 -6 -14 0\n-8 -7 19 0\n19 16 -11 0\n5 20 -18 0\n15 20 -12 0\n1 5 9 0\n8 -7 5 0\n-10 -12 20 0\n1 13 10 0\n```",
    "benchmark": null,
    "skill_refs": [
      {
        "skill_version_id": "skv_0xliguhu60",
        "requirement": "required"
      }
    ],
    "verifier_contract_id": "vct_wacbq9qe4y",
    "verifier_input_bindings": [
      {
        "key": "instance",
        "content_hash": "sha256:eef24648920b3ca871342d0b1554341c350de9bf3ec1230aa0b4a578a6ced3cf",
        "size_bytes": 1066,
        "media_type": "text/plain"
      }
    ],
    "sealing": null
  },
  "verifier_contract": {
    "id": "vct_wacbq9qe4y",
    "title": "Satisfying assignment for the bound CNF instance",
    "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.",
    "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"
      }
    ],
    "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_xdh2822hya",
    "revision": "/api/problems/prb_xdh2822hya/revisions/1",
    "mcp": "start_attempt {\"problem\":\"sat-dogfood-small\",\"revision\":1,\"provenance\":\"mixed\"}"
  }
}