In mathematical logic, given an unsatisfiable Boolean propositional formula in conjunctive normal form, a subset of clauses whose conjunction is still unsatisfiable is called an unsatisfiable core of the original formula. Many SAT solvers can produce a resolution graph which proves the unsatisfiability of the original problem.
In mathematical logic, given an unsatisfiable Boolean propositional formula in conjunctive normal form, a subset of clauses whose conjunction is still unsatisfiable is called an unsatisfiable core of the original formula. Many SAT solvers can produce a resolution graph which proves the unsatisfiability of the original problem.
Source: Wikipedia "Unsatisfiable core" · CC BY-SA 4.0
Share this article: X · Bluesky