SAT Solver Dogfood

Purpose

This Campaign exists to exercise TfP's own plumbing — Campaign → Problem → immutable ProblemRevision → pinned SkillVersion → MCP discovery and delivery → Attempt → Submission → automatic Verification — with tasks whose results are simple and machine-checkable.

It is explicitly a dogfood / integration fixture, not a claim that these are unsolved research Problems. Each Problem embeds a satisfiable DIMACS CNF instance and asks for a satisfying assignment. The pinned @tfp/sat-solving Skill explains the format, the expected assignment representation, how to check a result locally, and how to submit.

Each Problem's revision pins the @tfp/sat-assignment VerifierContract and binds its CNF instance as the Contract's instance reference input, so every Submission is verified automatically in TfP's sandbox.