Satisfy a medium 3-SAT instance (100 variables)

{
  "problem": {
    "id": "prb_80gusf4yx9",
    "slug": "sat-dogfood-medium",
    "title": "Satisfy a medium 3-SAT instance (100 variables)",
    "structure": "SOLVE",
    "status": "archived",
    "campaign": "sat-solver-dogfood",
    "summary": "Produce a satisfying assignment for a medium TfP-generated DIMACS CNF instance: 100 variables, 430 clauses. Any ordinary SAT solver handles this instantly."
  },
  "revision": {
    "id": "prv_q3d2dd9sfk",
    "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 `202`, 100 variables, 430 clauses). Not a research benchmark; satisfiability is guaranteed by construction.\n- SHA-256 of the CNF text below: `5290b83c69d5c5a69eb32f32f3965aca66e80de4f12659340883d230fa6c8156` — 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=202)\np cnf 100 430\n37 73 -36 0\n47 -65 35 0\n-46 6 9 0\n-19 -64 -42 0\n-69 -55 -87 0\n57 -63 -62 0\n94 36 -68 0\n-52 -88 -100 0\n74 -4 -43 0\n-73 -29 -38 0\n-100 -18 -81 0\n-34 80 44 0\n74 -4 80 0\n-46 31 11 0\n-69 -85 -81 0\n-25 96 -38 0\n88 -51 -25 0\n70 -28 19 0\n26 41 19 0\n73 84 74 0\n69 -71 -34 0\n-28 -48 49 0\n15 10 69 0\n-2 21 -24 0\n-32 86 3 0\n-14 -79 -98 0\n33 -41 -58 0\n-65 -27 63 0\n-13 21 19 0\n82 -66 29 0\n-76 20 -19 0\n-4 86 3 0\n-21 61 58 0\n-56 92 71 0\n54 -30 -76 0\n-93 -16 -81 0\n3 76 -92 0\n-27 3 36 0\n86 -30 -88 0\n73 -7 -64 0\n-67 -19 1 0\n61 69 -16 0\n-40 98 26 0\n86 23 -42 0\n23 -82 -38 0\n72 4 -92 0\n56 78 -81 0\n-25 -92 3 0\n-27 -67 90 0\n40 -56 -42 0\n57 -77 -50 0\n74 93 -71 0\n-93 15 26 0\n1 -29 -63 0\n39 -50 -67 0\n80 -33 3 0\n96 -69 98 0\n26 -18 -58 0\n-50 -37 62 0\n-42 66 89 0\n62 -25 -30 0\n-22 51 -98 0\n-38 -15 -97 0\n86 -40 -38 0\n-59 91 89 0\n60 87 -37 0\n78 21 55 0\n2 25 -66 0\n81 75 88 0\n-40 63 59 0\n28 6 -48 0\n44 -62 59 0\n70 45 -27 0\n-40 49 -73 0\n-79 10 -59 0\n31 10 37 0\n-99 -30 7 0\n-52 89 63 0\n3 71 -38 0\n-21 -50 -55 0\n-64 23 -22 0\n4 91 72 0\n-76 56 74 0\n19 90 85 0\n-4 -30 19 0\n35 -7 78 0\n28 -46 -90 0\n-79 -81 73 0\n-79 -33 80 0\n-64 -34 23 0\n80 22 -64 0\n99 94 -69 0\n24 -12 -84 0\n-95 6 58 0\n19 -58 -7 0\n66 54 33 0\n-70 10 -73 0\n17 37 36 0\n-14 6 -28 0\n-60 -69 14 0\n30 100 60 0\n-45 57 73 0\n-45 -64 36 0\n-28 59 98 0\n-75 -36 -98 0\n-39 -88 68 0\n-70 -45 47 0\n44 -2 -72 0\n92 64 -34 0\n19 47 -56 0\n-57 74 -11 0\n-94 23 -49 0\n44 -65 -61 0\n-66 81 -44 0\n-68 -13 57 0\n-7 -9 6 0\n-54 -34 29 0\n11 -46 -68 0\n-2 -72 75 0\n-79 100 15 0\n-66 27 11 0\n-78 65 -79 0\n-91 43 -56 0\n-49 -34 -30 0\n-69 -14 57 0\n36 37 45 0\n-47 -49 -18 0\n45 39 -28 0\n-60 97 -75 0\n-32 -54 15 0\n-82 76 -48 0\n-55 3 -21 0\n-55 -71 17 0\n-21 -76 47 0\n-21 -100 23 0\n1 13 71 0\n5 -37 90 0\n-69 47 -5 0\n-46 -42 -68 0\n-14 80 7 0\n-99 -58 -89 0\n-2 -63 53 0\n-42 80 4 0\n7 55 -39 0\n61 -27 -53 0\n11 -1 -23 0\n-65 -37 -45 0\n80 93 83 0\n76 93 -54 0\n66 -38 -30 0\n68 -94 39 0\n-56 -31 63 0\n17 -60 -2 0\n33 -82 -64 0\n-44 -62 -56 0\n-16 -92 31 0\n-62 -85 -25 0\n89 -69 -39 0\n-75 -74 -25 0\n87 -12 -3 0\n-5 57 80 0\n11 3 -78 0\n-52 18 71 0\n10 -97 11 0\n81 15 30 0\n-79 54 18 0\n64 -39 -56 0\n88 -49 27 0\n-75 95 -91 0\n-45 20 -22 0\n3 77 -9 0\n-69 92 73 0\n-100 63 96 0\n78 85 9 0\n-58 -86 4 0\n-40 99 -90 0\n5 -2 6 0\n-10 1 93 0\n-43 65 -22 0\n-21 87 -95 0\n-76 -52 69 0\n-12 63 -30 0\n39 33 -91 0\n-38 25 68 0\n84 96 42 0\n-12 51 -11 0\n-55 -26 -79 0\n-79 30 -74 0\n68 -41 -31 0\n18 88 97 0\n28 90 63 0\n-19 5 2 0\n-47 -71 7 0\n24 89 20 0\n43 -73 -29 0\n38 47 88 0\n-59 14 93 0\n66 -64 26 0\n-32 22 50 0\n-38 -25 96 0\n-79 37 10 0\n-36 15 21 0\n22 85 -34 0\n-45 91 34 0\n-60 -48 19 0\n-63 31 -82 0\n96 74 55 0\n57 -73 28 0\n21 -67 83 0\n4 -93 -19 0\n8 -71 77 0\n-56 -14 25 0\n-68 25 1 0\n50 60 98 0\n11 97 -59 0\n-77 -15 -86 0\n6 31 -38 0\n-89 -30 -58 0\n63 -43 1 0\n26 72 -50 0\n74 -54 -53 0\n75 -32 -2 0\n-63 -77 -80 0\n-51 15 38 0\n41 -77 -12 0\n-4 -49 8 0\n-21 87 -30 0\n-13 79 -28 0\n-40 18 24 0\n28 -100 -81 0\n-51 -83 85 0\n42 36 -98 0\n-94 -14 -9 0\n8 -66 17 0\n-81 61 -55 0\n-30 23 -7 0\n55 61 31 0\n79 15 64 0\n47 78 -68 0\n-59 -99 31 0\n26 -59 -25 0\n-61 -15 -39 0\n1 19 49 0\n17 92 98 0\n-20 35 19 0\n91 10 -42 0\n-32 30 21 0\n-100 -2 -93 0\n17 -4 -40 0\n8 -71 -14 0\n-13 -43 90 0\n4 51 -98 0\n35 -76 46 0\n-40 1 20 0\n36 82 34 0\n89 -21 4 0\n63 -25 49 0\n-38 -92 -84 0\n47 -85 49 0\n70 22 -67 0\n14 -89 -48 0\n28 12 -52 0\n-1 4 72 0\n-39 86 52 0\n98 -47 -44 0\n78 28 -30 0\n79 -83 -56 0\n-39 1 -27 0\n75 59 -34 0\n95 -53 -93 0\n-61 19 -78 0\n83 -63 9 0\n-39 25 -23 0\n-81 -16 57 0\n-75 -25 16 0\n-21 38 -7 0\n-25 36 -12 0\n73 51 12 0\n74 -27 54 0\n-82 -79 -80 0\n-59 -50 57 0\n-68 64 -38 0\n60 25 37 0\n-33 -30 -65 0\n51 24 -21 0\n-48 -26 37 0\n-45 55 30 0\n-52 -76 -70 0\n84 -46 45 0\n100 -58 34 0\n33 8 6 0\n-67 18 4 0\n-49 -15 -39 0\n54 -45 88 0\n-46 -81 13 0\n-96 19 -85 0\n8 74 29 0\n-70 43 -42 0\n-13 -17 21 0\n-24 26 63 0\n26 -40 -49 0\n-37 -79 93 0\n83 -25 -3 0\n49 -64 -33 0\n-99 98 7 0\n-81 -53 -8 0\n-70 -83 5 0\n40 49 -34 0\n27 39 6 0\n-12 -69 19 0\n36 46 -51 0\n89 -54 37 0\n49 93 67 0\n27 81 84 0\n-48 97 69 0\n-100 -29 7 0\n27 -15 -62 0\n-80 -41 58 0\n71 23 -56 0\n-8 -64 96 0\n70 -48 10 0\n-29 -62 -53 0\n10 -58 -81 0\n-16 -30 -58 0\n-69 21 -77 0\n-34 -29 -17 0\n-78 -41 -16 0\n15 -64 88 0\n-6 -50 72 0\n12 -73 -32 0\n19 -51 -74 0\n-63 -50 -61 0\n37 100 -80 0\n-77 -69 -45 0\n20 -33 44 0\n63 -45 -68 0\n-48 -62 -59 0\n-48 -57 -96 0\n-29 17 77 0\n-4 -13 93 0\n-75 8 69 0\n-6 71 -52 0\n-38 67 47 0\n12 63 84 0\n-59 97 45 0\n5 99 -12 0\n31 -7 -10 0\n-38 -83 71 0\n39 -98 -55 0\n-54 13 -100 0\n-5 -28 -39 0\n86 87 -21 0\n32 80 11 0\n37 10 -1 0\n-60 -28 100 0\n-72 26 88 0\n-14 20 50 0\n39 -47 98 0\n-8 1 -16 0\n78 38 -91 0\n-70 54 8 0\n-69 -71 18 0\n-48 -51 63 0\n39 37 55 0\n89 -27 -32 0\n-79 -5 -27 0\n-68 -12 44 0\n36 35 -38 0\n47 -69 -35 0\n-92 1 -95 0\n-14 7 60 0\n-22 -75 -32 0\n91 49 51 0\n13 74 -28 0\n63 -62 -2 0\n1 100 -79 0\n80 16 99 0\n67 63 -83 0\n-39 22 -34 0\n45 -39 -91 0\n61 -32 91 0\n43 -100 80 0\n-57 -92 -5 0\n-88 25 -12 0\n-80 -91 23 0\n33 -14 15 0\n31 10 -53 0\n-84 65 -42 0\n41 -30 81 0\n-79 -51 32 0\n31 13 -79 0\n82 -48 51 0\n88 81 -21 0\n14 15 -4 0\n85 24 75 0\n-28 16 -59 0\n-61 -12 -2 0\n44 74 61 0\n10 9 6 0\n-80 -100 73 0\n54 55 -43 0\n49 2 44 0\n-79 44 -52 0\n89 47 24 0\n-69 88 -16 0\n-57 93 -27 0\n44 -51 -85 0\n-32 37 -99 0\n81 -34 -79 0\n10 -63 -40 0\n18 24 81 0\n-92 -79 41 0\n46 23 60 0\n-27 53 -58 0\n-68 1 -15 0\n34 -82 -79 0\n-89 24 -2 0\n-14 56 -41 0\n-80 -39 5 0\n-88 -27 12 0\n-94 97 -4 0\n-48 -72 -36 0\n6 36 68 0\n73 96 -11 0\n-8 -90 86 0\n23 -20 -10 0\n35 95 67 0\n15 -8 -59 0\n-14 41 -21 0\n-63 84 24 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:5290b83c69d5c5a69eb32f32f3965aca66e80de4f12659340883d230fa6c8156",
        "size_bytes": 5366,
        "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_80gusf4yx9",
    "revision": "/api/problems/prb_80gusf4yx9/revisions/1",
    "mcp": "start_attempt {\"problem\":\"sat-dogfood-medium\",\"revision\":1,\"provenance\":\"mixed\"}"
  }
}