Proof minimization formulas dataset
收藏NIAID Data Ecosystem2026-05-02 收录
下载链接：
https://zenodo.org/record/14052282
下载链接
链接失效反馈官方服务：
资源简介：
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:
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.
proofmin-sat-competition-2002: a subset of unsatisfiable SAT Competition 2002 formulas solved within 15 seconds with an addition of their subsets produced by MUSer2.
创建时间：
2024-11-11
