# Trimming Graphs Using Clausal Proof Optimization

## TL;DR

This paper introduces a proof-based method to iteratively trim propositional formulas to find smaller unsatisfiable cores, demonstrated by reducing a complex graph's size while maintaining its chromatic properties.

## Contribution

It proposes a novel proof minimization technique that delays clause deletion, leading to smaller unsatisfiable cores compared to existing methods.

## Key findings

- Reduced the known minimal unit-distance graph from 553 to 529 vertices.
- Decreased the number of edges in the graph from 2720 to 2670.
- Showed the effectiveness of proof-based trimming in graph reduction.

## Abstract

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 2720 edges to 529 vertices and 2670 edges.