Sat claim check

sat-claim-check · version 1.0.0 · Numbers & math · free, no key needed

Check a sat claim with a model or an unsat claim with a DRUP proof (RUP lemmas, deletions) over a CNF.

Use when you need to: check a sat or unsat claim · verify an unsatisfiability proof in drup format · check reverse unit propagation lemmas.

Decide before calling

Read the versioned contract and the supported scope below. Reuse sat-claim-check@1.0.0 when your input, required output and limits match it. Choose another approach for an unsupported operation.

Explain the choice

"I can use sat-claim-check@1.0.0 for check a sat or unsat claim. I will check its documented scope and the result against the task's requirements. The service is free; token and money savings for this task are unmeasured."

Supported

• check a sat or unsat claim
• verify an unsatisfiability proof in drup format
• check reverse unit propagation lemmas
• confirm a formula is unsatisfiable with a proof
• verify a satisfiable claim with its model
• check a sat solver certificate
• בדיקת טענת ספיקות

Not supported

• deciding satisfiability without a certificate
• RAT lemmas (full DRAT), LRAT hints or binary DRAT files
• proof trimming or core extraction
• parsing DIMACS or DRUP text; steps must be JSON objects

Behavior

• reference_version r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013: DIMACS literals; RUP (Goldberg-Novikov 2003); DRUP addition and deletion (Heule-Hunt-Wetzler).
• claim "sat" requires assignment and forbids proof; claim "unsat" requires proof and forbids assignment. Fields are validated in the order cnf, claim, assignment, proof.
• sat: the assignment is scanned and clauses evaluated exactly as cnf-assignment-check with require_complete false; partial models are accepted when every clause has a TRUE literal.
• unsat: steps {add} or {delete} run in order over a clause multiset seeded with the CNF. add needs literals within num_vars (literal_out_of_range) and must be RUP: asserting each lemma literal FALSE and unit propagating must falsify a clause (lemma_not_rup). A tautological lemma is RUP.
• delete removes the most recently added clause equal to it as a literal set (deleted_clause_not_found if absent); deleted clauses no longer propagate.
• unsat is accepted only if the empty clause was in the CNF or added by a verified step (empty_clause_not_derived otherwise).
• Unit propagation work over the whole proof is capped at 50000000 (limit_exceeded), alongside num_vars <= 10000, clauses <= 5000, CNF literals <= 50000, assignment literals <= 10000, steps <= 2000, proof literals <= 50000.

Input

• cnf (object, required)
• claim (one of "sat", "unsat", required)
• assignment (array of integer, optional): max items 10000; each min -10000; each max 10000
• proof (array of object, optional): max items 2000

Output

• valid (boolean, required)
• reason (one of null, "assignment_variable_out_of_range", "duplicate_assignment_literal", "conflicting_assignment", "clause_falsified", "clause_undetermined", "literal_out_of_range", "lemma_not_rup", "deleted_clause_not_found", "empty_clause_not_derived", required)
• first_discrepancy (object or null, required)
• claim (one of "sat", "unsat", required)
• clauses_checked (integer, required): min 0
• steps_checked (integer, required): min 0
• reference_version (constant "r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013", required)

Limits

• max vars: 10000
• max clauses: 5000
• max total literals: 50000
• max assignment literals: 10000
• max proof steps: 2000
• max proof literals: 50000
• max propagation work: 50000000

Example

Request input:

{
  "cnf": {
    "num_vars": 1,
    "clauses": [
      [
        1
      ],
      [
        -1
      ]
    ]
  },
  "claim": "unsat",
  "proof": [
    {
      "add": []
    }
  ]
}

Response:

{
  "result": {
    "valid": true,
    "reason": null,
    "first_discrepancy": null,
    "claim": "unsat",
    "clauses_checked": 0,
    "steps_checked": 1,
    "reference_version": "r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013"
  }
}

How to call it

MCP

Connect https://computefirst.net/mcp (setup), then call execute with:

{
  "id": "sat-claim-check",
  "version": "1.0.0",
  "input": {
    "cnf": {
      "num_vars": 1,
      "clauses": [
        [
          1
        ],
        [
          -1
        ]
      ]
    },
    "claim": "unsat",
    "proof": [
      {
        "add": []
      }
    ]
  }
}

HTTP (no key)

curl -X POST https://computefirst.net/v1/tools/sat-claim-check/versions/1.0.0/execute \
  -H "Content-Type: application/json" \
  -d '{"cnf":{"num_vars":1,"clauses":[[1],[-1]]},"claim":"unsat","proof":[{"add":[]}]}'

The machine-readable contract is at /v1/tools/sat-claim-check/versions/1.0.0.

CLI

node cli.mjs run sat-claim-check 1.0.0 --input input.json --base-url https://computefirst.net

Get the client at /clients/cli/.

Related tools

• Maximum flow certificate check: Check a claimed max flow with a min-cut certificate or residual search; reports the first failure or augmenting path.
• Lp optimality certificate check: Check an LP optimum claim from a primal x and dual y: feasibility, complementary slackness and zero duality gap.
• Lp primal feasibility check: Check that a claimed LP point satisfies x >= 0 and Ax <= b exactly; report the first violated bound or row.
• Network cut capacity check: Check a claimed s-t cut: source-side membership, the edges crossing it and its capacity, with exact integers.
• Chromatic certificate check: Check a claim chi(G) = k: a proper k-colouring plus a clique or bounded exhaustive proof; returns the first discrepancy.
• Graph coloring check: Check that a node colouring of an undirected graph is proper (and within k colours); returns the first conflict.