تقرير
Even shorter proofs without new variables
| العنوان: | Even shorter proofs without new variables |
|---|---|
| المؤلفون: | Rebola-Pardo, Adrián |
| سنة النشر: | 2023 |
| المجموعة: | Computer Science |
| مصطلحات موضوعية: | Computer Science - Logic in Computer Science |
| الوصف: | Proof formats for SAT solvers have diversified over the last decade, enabling new features such as extended resolution-like capabilities, very general extension-free rules, inclusion of proof hints, and pseudo-boolean reasoning. Interference-based methods have been proven effective, and some theoretical work has been undertaken to better explain their limits and semantics. In this work, we combine the subsumption redundancy notion from (Buss, Thapen 2019) and the overwrite logic framework from (Rebola-Pardo, Suda 2018). Natural generalizations then become apparent, enabling even shorter proofs of the pigeonhole principle (compared to those from (Heule, Kiesl, Biere 2017)) and smaller unsatisfiable core generation. Comment: 21 pages |
| نوع الوثيقة: | Working Paper |
| URL الوصول: | http://arxiv.org/abs/2307.12098 |
| رقم الأكسشن: | edsarx.2307.12098 |
| قاعدة البيانات: | arXiv |
| الوصف غير متاح. |