# 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](/v1/tools/sat-claim-check/versions/1.0.0) 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:

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

Response:

```json
{
  "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](/docs#connect)), then call `execute` with:

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

### HTTP (no key)

```sh
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](/v1/tools/sat-claim-check/versions/1.0.0).

### CLI

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

Get the client at [/clients/cli/](/clients/cli/).

## Related tools

- [Maximum flow certificate check](/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](/tools/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](/tools/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](/tools/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](/tools/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](/tools/graph-coloring-check): Check that a node colouring of an undirected graph is proper (and within k colours); returns the first conflict.