An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle
It has been proven that extended resolution (ER) has more powerful reasoning than general resolution for the pigeonhole principle in Cook’s paper. This fact indicates the possibility that a solver based on extended resolution can exceed Boolean satisfiability problem solvers (SAT solvers for short)...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2022-12-01
|
| Series: | Algorithms |
| Subjects: | |
| Online Access: | https://www.mdpi.com/1999-4893/15/12/479 |
| _version_ | 1797461818160971776 |
|---|---|
| author | Tomohiro Sonobe |
| author_facet | Tomohiro Sonobe |
| author_sort | Tomohiro Sonobe |
| collection | DOAJ |
| description | It has been proven that extended resolution (ER) has more powerful reasoning than general resolution for the pigeonhole principle in Cook’s paper. This fact indicates the possibility that a solver based on extended resolution can exceed Boolean satisfiability problem solvers (SAT solvers for short) based on general resolution. However, few studies have provided practical evidence of this assumption. This paper explores how extended resolution can improve SAT solvers by using the pigeonhole principle, which was the first problem solved by ER in polynomial steps. In fact, although Cook’s paper introduced how to add auxiliary variables, there is no evidence that these variables are really useful for practical solvers. We try to answer the question: If the SAT solver can add appropriate auxiliary variables as proposed in Cook’s paper, can the solver enhance its performance by utilizing these variables? Experimental results show that if the solver properly prioritizes the extended variables in the search, the solver can end the search in a shorter time. |
| first_indexed | 2024-03-09T17:24:47Z |
| format | Article |
| id | doaj.art-30b4f22936a24915908d0466be9f4193 |
| institution | Directory Open Access Journal |
| issn | 1999-4893 |
| language | English |
| last_indexed | 2024-03-09T17:24:47Z |
| publishDate | 2022-12-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Algorithms |
| spelling | doaj.art-30b4f22936a24915908d0466be9f41932023-11-24T12:49:35ZengMDPI AGAlgorithms1999-48932022-12-01151247910.3390/a15120479An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole PrincipleTomohiro Sonobe0National Institute of Informatics, 2-1-2 Hitotsubashi, Chiyoda-ku, Tokyo 101-8430, JapanIt has been proven that extended resolution (ER) has more powerful reasoning than general resolution for the pigeonhole principle in Cook’s paper. This fact indicates the possibility that a solver based on extended resolution can exceed Boolean satisfiability problem solvers (SAT solvers for short) based on general resolution. However, few studies have provided practical evidence of this assumption. This paper explores how extended resolution can improve SAT solvers by using the pigeonhole principle, which was the first problem solved by ER in polynomial steps. In fact, although Cook’s paper introduced how to add auxiliary variables, there is no evidence that these variables are really useful for practical solvers. We try to answer the question: If the SAT solver can add appropriate auxiliary variables as proposed in Cook’s paper, can the solver enhance its performance by utilizing these variables? Experimental results show that if the solver properly prioritizes the extended variables in the search, the solver can end the search in a shorter time.https://www.mdpi.com/1999-4893/15/12/479searchSAT solverextended resolution |
| spellingShingle | Tomohiro Sonobe An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle Algorithms search SAT solver extended resolution |
| title | An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle |
| title_full | An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle |
| title_fullStr | An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle |
| title_full_unstemmed | An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle |
| title_short | An Experimental Survey of Extended Resolution Effects for SAT Solvers on the Pigeonhole Principle |
| title_sort | experimental survey of extended resolution effects for sat solvers on the pigeonhole principle |
| topic | search SAT solver extended resolution |
| url | https://www.mdpi.com/1999-4893/15/12/479 |
| work_keys_str_mv | AT tomohirosonobe anexperimentalsurveyofextendedresolutioneffectsforsatsolversonthepigeonholeprinciple AT tomohirosonobe experimentalsurveyofextendedresolutioneffectsforsatsolversonthepigeonholeprinciple |