We present a method to gradually compute a smaller and smaller unsatisfiable core of a propositional formula by minimizing proofs of unsatisfiability. The goal is to compute a minimal unsatisfiable core that is relatively small compared to other minimal unsatisfiable cores of the same formula. We try to achieve this goal by postponing deletion of arbitrary clauses from the formula as long as possible—in contrast to existing minimal unsatisfiable core algorithms. We applied this method to reduce the smallest known unit-distance graph with chromatic number 5 from 553 vertices and edges to 529 vertices and edges.
CITATION STYLE
Heule, M. J. H. (2019). Trimming Graphs Using Clausal Proof Optimization. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11802 LNCS, pp. 251–267). Springer. https://doi.org/10.1007/978-3-030-30048-7_15
Mendeley helps you to discover research relevant for your work.