{"id":"cnf-assignment-check","version":"1.0.0","description":"Check a claimed truth assignment against a DIMACS-style CNF; report the first bad literal or unsatisfied clause.","supported_operations":["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"],"unsupported_operations":["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"],"semantics":["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)."],"limits":{"max_vars":10000,"max_clauses":5000,"max_total_literals":50000,"max_assignment_literals":10000},"pricing":{"status":"unpriced","charge_usd":null},"input_schema":{"type":"object","additionalProperties":false,"required":["cnf","assignment"],"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}}}}},"assignment":{"type":"array","maxItems":10000,"items":{"type":"integer","minimum":-10000,"maximum":10000}},"require_complete":{"type":"boolean"}}},"output_schema":{"type":"object","additionalProperties":false,"required":["valid","reason","first_discrepancy","clauses_checked","reference_version"],"properties":{"valid":{"type":"boolean"},"reason":{"type":["string","null"],"enum":[null,"assignment_variable_out_of_range","duplicate_assignment_literal","conflicting_assignment","incomplete_assignment","clause_falsified","clause_undetermined"]},"first_discrepancy":{"type":["object","null"],"additionalProperties":false,"required":["kind"],"properties":{"kind":{"type":"string","enum":["assignment","variable","clause"]},"assignment_index":{"type":"integer","minimum":0},"literal":{"type":"integer"},"previous_index":{"type":"integer","minimum":0},"variable":{"type":"integer","minimum":1},"clause_index":{"type":"integer","minimum":0},"clause":{"type":"array","items":{"type":"integer"}},"unassigned_literals":{"type":"array","items":{"type":"integer"}}}},"clauses_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":3,"clauses":[[1,-2],[-1,2,3],[-1]]},"assignment":[-1,-2]},"output":{"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"}},{"input":{"cnf":{"num_vars":1,"clauses":[[1],[-1]]},"assignment":[1]},"output":{"valid":false,"reason":"clause_falsified","first_discrepancy":{"kind":"clause","clause_index":1,"clause":[-1]},"clauses_checked":2,"reference_version":"r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013"}},{"input":{"cnf":{"num_vars":2,"clauses":[[1]]},"assignment":[1,-2,-1]},"output":{"valid":false,"reason":"conflicting_assignment","first_discrepancy":{"kind":"assignment","assignment_index":2,"literal":-1,"previous_index":0},"clauses_checked":0,"reference_version":"r71-sat-1.0.0+dimacs-cnf-1993+resolution-robinson-1965+drup-2013"}}],"execute_url":"/v1/tools/cnf-assignment-check/versions/1.0.0/execute"}