Cnf assignment check

cnf-assignment-check · version 1.0.0 · Numbers & math · free, no key needed

Check a claimed truth assignment against a DIMACS-style CNF; report the first bad literal or unsatisfied clause.

Use when you need to: check a sat assignment against cnf clauses · verify a truth assignment satisfies a cnf formula · which clause does this assignment violate.

Decide before calling

Read the versioned contract and the supported scope below. Reuse cnf-assignment-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 cnf-assignment-check@1.0.0 for check a sat assignment against cnf clauses. 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 assignment against cnf clauses
• verify a truth assignment satisfies a cnf formula
• which clause does this assignment violate
• validate a dimacs model line against the formula
• check boolean variable assignment for a cnf
• find the first unsatisfied clause
• בדיקת השמה לנוסחת CNF

Not supported

• finding a satisfying assignment (solving SAT)
• parsing DIMACS text files; clauses must be JSON integer arrays
• checking unsatisfiability proofs (use resolution-proof-check or sat-claim-check)
• MaxSAT weights, XOR clauses or quantified formulas

Behavior

• reference_version r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013: DIMACS literal convention (v TRUE, -v FALSE, variables 1..num_vars).
• Assignment scan in index order: literal above num_vars -> assignment_variable_out_of_range; repeated literal -> duplicate_assignment_literal; opposite literal -> conflicting_assignment (previous_index is the earlier entry).
• require_complete is optional (omitted = false); when true, the smallest unassigned variable is reported as incomplete_assignment before clauses are evaluated.
• Clauses are evaluated in input order; a clause holds only if some literal is assigned TRUE. The first failing clause is clause_falsified (all literals FALSE, including the empty clause) or clause_undetermined (no TRUE literal, some unassigned).
• clauses_checked counts clauses evaluated up to and including the failing one (all clauses when valid; 0 for assignment discrepancies).
• CNF literals must be non-zero integers within num_vars (invalid_input otherwise); assignment literals must be non-zero integers with absolute value at most 10000.
• Limits are checked before content: num_vars <= 10000, clauses <= 5000, CNF literals <= 50000, assignment literals <= 10000 (limit_exceeded).

Input

• cnf (object, required)
• assignment (array of integer, required): max items 10000; each min -10000; each max 10000
• require_complete (boolean, optional)

Output

• valid (boolean, required)
• reason (one of null, "assignment_variable_out_of_range", "duplicate_assignment_literal", "conflicting_assignment", "incomplete_assignment", "clause_falsified", "clause_undetermined", required)
• first_discrepancy (object or null, required)
• clauses_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

Example

Request input:

{
  "cnf": {
    "num_vars": 3,
    "clauses": [
      [
        1,
        -2
      ],
      [
        -1,
        2,
        3
      ],
      [
        -1
      ]
    ]
  },
  "assignment": [
    -1,
    -2
  ]
}

Response:

{
  "result": {
    "valid": true,
    "reason": null,
    "first_discrepancy": null,
    "clauses_checked": 3,
    "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": "cnf-assignment-check",
  "version": "1.0.0",
  "input": {
    "cnf": {
      "num_vars": 3,
      "clauses": [
        [
          1,
          -2
        ],
        [
          -1,
          2,
          3
        ],
        [
          -1
        ]
      ]
    },
    "assignment": [
      -1,
      -2
    ]
  }
}

HTTP (no key)

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

The machine-readable contract is at /v1/tools/cnf-assignment-check/versions/1.0.0.

CLI

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

Get the client at /clients/cli/.

Related 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 flow feasibility check: Check a claimed s-t flow for capacity bounds and conservation with exact integers; returns the first bad edge or node.
• Resolution proof check: Check each binary resolution step (antecedents, pivot, resolvent) of a proof over a CNF; report the first bad step.
• Topological order check: Check that a claimed vertex order is a permutation and topological order of a digraph; reports the first backward edge
• Chi square decomposition check: Check a claimed Pearson chi-square, its per-cell (O-E)^2/E terms and df exactly; returns the first wrong term.
• Graph coloring check: Check that a node colouring of an undirected graph is proper (and within k colours); returns the first conflict.