Finding the Hardest Formulas for Resolution
| Autor: | Tomáš Peitl, Stefan Szeider |
|---|---|
| Rok vydání: | 2020 |
| Předmět: |
Discrete mathematics
050101 languages & linguistics 05 social sciences Resolution (electron density) 02 engineering and technology Limiting Computer Science::Computational Complexity TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Computer Science::Logic in Computer Science Scheme (mathematics) Encoding (memory) 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Symmetry breaking Mathematics |
| Zdroj: | Lecture Notes in Computer Science ISBN: 9783030584740 CP |
| DOI: | 10.1007/978-3-030-58475-7_30 |
| Popis: | A CNF formula is harder than another CNF formula with the same number of clauses if it requires a longer resolution proof. The resolution hardness numbers give for \(m=1,2,\dots \) the length of a shortest proof of a hardest formula on m clauses. We compute the first ten resolution hardness numbers, along with the corresponding hardest formulas. We achieve this by a candidate filtering and symmetry breaking search scheme for limiting the number of potential candidates for formulas and an efficient SAT encoding for computing a shortest resolution proof of a given candidate formula. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|