Proof minimization formulas dataset
收藏官方服务：
资源简介：
The collection of formulas used for the experimental evaluation in "How to discover short, shorter, and the shortest proofs of unsatisfiability: a branch-and-bound approach for resolution proof length minimization." Directory structure for synthetic.zip: full: synthetic formulas, including the random 3-CNFs, random graph coloring, and SMUs from Peitl & Szeider (2021). small and small-opt: collections with the same structure but smaller and without the SMUs; small-opt additionally excludes everything except 3-CNFs. competition.zip contains the UNSAT formulas from SAT Competitions until 2025 that have been solved within fifteen seconds by CaDiCaL.
提供机构：
Zenodo创建时间：
2026-03-03
