{"id":"sat-claim-check","version":"1.0.0","description":"Check a sat claim with a model or an unsat claim with a DRUP proof (RUP lemmas, deletions) over a CNF.","supported_operations":["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","בדיקת טענת ספיקות"],"unsupported_operations":["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"],"semantics":["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."],"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},"pricing":{"status":"unpriced","charge_usd":null},"input_schema":{"type":"object","additionalProperties":false,"required":["cnf","claim"],"properties":{"cnf":{"type":"object","additionalProperties":false,"required":["num_vars","clauses"],"properties":{"num_vars":{"type":"integer","minimum":0,"maximum":10000},"clauses":{"type":"array","maxItems":5000,"items":{"type":"array","items":{"type":"integer","minimum":-10000,"maximum":10000}}}}},"claim":{"type":"string","enum":["sat","unsat"]},"assignment":{"type":"array","maxItems":10000,"items":{"type":"integer","minimum":-10000,"maximum":10000}},"proof":{"type":"array","maxItems":2000,"items":{"type":"object","additionalProperties":false,"minProperties":1,"maxProperties":1,"properties":{"add":{"type":"array","items":{"type":"integer","minimum":-10000,"maximum":10000}},"delete":{"type":"array","items":{"type":"integer","minimum":-10000,"maximum":10000}}}}}}},"output_schema":{"type":"object","additionalProperties":false,"required":["valid","reason","first_discrepancy","claim","clauses_checked","steps_checked","reference_version"],"properties":{"valid":{"type":"boolean"},"reason":{"type":["string","null"],"enum":[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"]},"first_discrepancy":{"type":["object","null"],"additionalProperties":false,"required":["kind"],"properties":{"kind":{"type":"string","enum":["assignment","clause","step","conclusion"]},"assignment_index":{"type":"integer","minimum":0},"literal":{"type":"integer"},"previous_index":{"type":"integer","minimum":0},"clause_index":{"type":"integer","minimum":0},"clause":{"type":"array","items":{"type":"integer"}},"unassigned_literals":{"type":"array","items":{"type":"integer"}},"step_index":{"type":"integer","minimum":0},"step_count":{"type":"integer","minimum":0}}},"claim":{"type":"string","enum":["sat","unsat"]},"clauses_checked":{"type":"integer","minimum":0},"steps_checked":{"type":"integer","minimum":0},"reference_version":{"type":"string","const":"r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013"}}},"examples":[{"input":{"cnf":{"num_vars":1,"clauses":[[1],[-1]]},"claim":"unsat","proof":[{"add":[]}]},"output":{"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"}},{"input":{"cnf":{"num_vars":2,"clauses":[[1,2]]},"claim":"unsat","proof":[{"add":[1]}]},"output":{"valid":false,"reason":"lemma_not_rup","first_discrepancy":{"kind":"step","step_index":0,"clause":[1]},"claim":"unsat","clauses_checked":0,"steps_checked":0,"reference_version":"r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013"}},{"input":{"cnf":{"num_vars":2,"clauses":[[1],[-2]]},"claim":"sat","assignment":[1,-2]},"output":{"valid":true,"reason":null,"first_discrepancy":null,"claim":"sat","clauses_checked":2,"steps_checked":0,"reference_version":"r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013"}}],"execute_url":"/v1/tools/sat-claim-check/versions/1.0.0/execute"}