{"id":"resolution-proof-check","version":"1.0.0","description":"Check each binary resolution step (antecedents, pivot, resolvent) of a proof over a CNF; report the first bad step.","supported_operations":["check a resolution proof","verify resolution refutation steps","validate a resolvent of two clauses","check that a proof derives the empty clause","find the first invalid resolution step","verify propositional resolution derivation","בדיקת הוכחת רזולוציה"],"unsupported_operations":["finding a resolution proof","first-order resolution with unification","hyper-resolution, weakening or multi-pivot steps","DRAT or RAT lemmas (sat-claim-check covers RUP/DRUP)"],"semantics":["reference_version r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013: Robinson binary resolution over DIMACS literals.","Clause ids: input clause i is id i; proof step s is id num_clauses + s; a step may cite only smaller ids.","Per step, in order: claimed literals within num_vars (literal_out_of_range); antecedent a then b available (antecedent_not_available); pivot within num_vars (pivot_out_of_range); pivot clashes (pivot_not_clashing) or, without a pivot, exactly one clashing variable (no_clashing_literal, ambiguous_pivot); claimed clause equals the resolvent as a set (resolvent_mismatch with canonical missing_literals and extra_literals).","Resolvent: if antecedent a holds p and b holds -p, (a minus p) union (b minus -p); otherwise (a minus -p) union (b minus p). Every copy is removed.","require_empty_clause is optional (omitted = true): the empty clause must appear among input clauses or proof steps, else empty_clause_not_derived.","empty_clause_id is the smallest id of an empty input clause or verified step (null if none); steps_checked counts verified steps before the first invalid one.","Limits: num_vars <= 10000, clauses <= 5000, CNF literals <= 50000, proof steps <= 2000, proof literals <= 50000, checked before literal content."],"limits":{"max_vars":10000,"max_clauses":5000,"max_total_literals":50000,"max_proof_steps":2000,"max_proof_literals":50000},"pricing":{"status":"unpriced","charge_usd":null},"input_schema":{"type":"object","additionalProperties":false,"required":["cnf","proof"],"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}}}}},"proof":{"type":"array","maxItems":2000,"items":{"type":"object","additionalProperties":false,"required":["clause","antecedents"],"properties":{"clause":{"type":"array","items":{"type":"integer","minimum":-10000,"maximum":10000}},"antecedents":{"type":"array","minItems":2,"maxItems":2,"items":{"type":"integer","minimum":0}},"pivot":{"type":"integer","minimum":1,"maximum":10000}}}},"require_empty_clause":{"type":"boolean"}}},"output_schema":{"type":"object","additionalProperties":false,"required":["valid","reason","first_discrepancy","steps_checked","empty_clause_id","reference_version"],"properties":{"valid":{"type":"boolean"},"reason":{"type":["string","null"],"enum":[null,"literal_out_of_range","antecedent_not_available","pivot_out_of_range","pivot_not_clashing","no_clashing_literal","ambiguous_pivot","resolvent_mismatch","empty_clause_not_derived"]},"first_discrepancy":{"type":["object","null"],"additionalProperties":false,"required":["kind"],"properties":{"kind":{"type":"string","enum":["step","conclusion"]},"step_index":{"type":"integer","minimum":0},"literal":{"type":"integer"},"antecedent":{"type":"integer","minimum":0},"pivot":{"type":"integer","minimum":1},"clashing_variables":{"type":"array","items":{"type":"integer","minimum":1}},"missing_literals":{"type":"array","items":{"type":"integer"}},"extra_literals":{"type":"array","items":{"type":"integer"}},"step_count":{"type":"integer","minimum":0}}},"steps_checked":{"type":"integer","minimum":0},"empty_clause_id":{"type":["integer","null"],"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":2,"clauses":[[1],[2],[-1,-2]]},"proof":[{"clause":[-2],"antecedents":[0,2],"pivot":1},{"clause":[],"antecedents":[1,3],"pivot":2}]},"output":{"valid":true,"reason":null,"first_discrepancy":null,"steps_checked":2,"empty_clause_id":4,"reference_version":"r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013"}},{"input":{"cnf":{"num_vars":2,"clauses":[[1,2],[-1,-2]]},"proof":[{"clause":[],"antecedents":[0,1]}]},"output":{"valid":false,"reason":"ambiguous_pivot","first_discrepancy":{"kind":"step","step_index":0,"clashing_variables":[1,2]},"steps_checked":0,"empty_clause_id":null,"reference_version":"r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013"}}],"execute_url":"/v1/tools/resolution-proof-check/versions/1.0.0/execute"}