True crafted formula families for benchmarking quantified satisfiability solvers. (English) Zbl 07810739
Dubois, Catherine (ed.) et al., Intelligent computer mathematics. 16th international conference, CICM 2023, Cambridge, UK, September 5–8, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14101, 291-296 (2023).
Summary: As the application of quantified Boolean formulas (QBF) continues to expand in various scientific and industrial domains, the development of efficient QBF solvers and their underlying proving strategies is of growing importance. To understand and to compare different solving approaches, techniques of proof complexity are applied. To this end, formula families have been crafted that exhibit certain properties of proof systems. These formulas are valuable to test and compare specific solver implementations. Traditionally, the focus is on false formulas, in this work we extend the formula generator QBFFam to produce true formulas based on two popular formula families from proof complexity.
For the entire collection see [Zbl 1531.68022].
For the entire collection see [Zbl 1531.68022].
MSC:
| 68Vxx | Computer science support for mathematical research and practice |
References:
| [1] | Balabanov, V.; Jiang, JR, Unified QBF certification and its applications, Formal Methods Syst. Des., 41, 1, 45-65 (2012) · Zbl 1284.68516 · doi:10.1007/s10703-012-0152-6 |
| [2] | Beyersdorff, O., Chew, L., Janota, M.: New resolution-based QBF calculi and their proof complexity. ACM Trans. Comput. Theory 11(4), 26:1-26:42 (2019) · Zbl 1496.68362 |
| [3] | Beyersdorff, O., Janota, M., Lonsing, F., Seidl, M.: Quantified Boolean formulas. In: Handbook of Satisfiability - Second Edition, pp. 1177-1221. IOS Press (2021) |
| [4] | Beyersdorff, O.; Pulina, L.; Seidl, M.; Shukla, A.; Li, C-M; Manyà, F., QBFFam: a tool for generating QBF families from proof complexity, Theory and Applications of Satisfiability Testing - SAT 2021, 21-29 (2021), Cham: Springer, Cham · Zbl 07495563 · doi:10.1007/978-3-030-80223-3_3 |
| [5] | Böhm, B., Peitl, T., Beyersdorff, O.: Should decisions in QCDCL follow prefix order? In: SAT. LIPIcs, vol. 236, pp. 11:1-11:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022) · Zbl 07880732 |
| [6] | Gelder, A.; Milano, M., Contributions to the theory of practical quantified Boolean formula solving, Principles and Practice of Constraint Programming, 647-663 (2012), Heidelberg: Springer, Heidelberg · Zbl 1390.68585 · doi:10.1007/978-3-642-33558-7_47 |
| [7] | Heule, M.; Järvisalo, M.; Lonsing, F.; Seidl, M.; Biere, A., Clause elimination for SAT and QSAT, J. Artif. Intell. Res., 53, 127-168 (2015) · Zbl 1336.68231 · doi:10.1613/jair.4694 |
| [8] | Janota, M.; Klieber, W.; Marques-Silva, J.; Clarke, E.; Cimatti, A.; Sebastiani, R., Solving QBF with counterexample guided refinement, Theory and Applications of Satisfiability Testing - SAT 2012, 114-128 (2012), Heidelberg: Springer, Heidelberg · Zbl 1273.68178 · doi:10.1007/978-3-642-31612-8_10 |
| [9] | Janota, M.; Marques-Silva, J.; Oliveira, E.; Gama, J.; Vale, Z.; Lopes Cardoso, H., An Achilles’ heel of term-resolution, Progress in Artificial Intelligence, 670-680 (2017), Cham: Springer, Cham · doi:10.1007/978-3-319-65340-2_55 |
| [10] | Kleine Büning, H., Lettmann, T.: Aussagenlogik: Deduktion und Algorithmen. Teubner (1994) · Zbl 0809.03003 |
| [11] | Lonsing, F.; Egly, U.; de Moura, L., DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL, Automated Deduction - CADE 26, 371-384 (2017), Cham: Springer, Cham · Zbl 1494.68288 · doi:10.1007/978-3-319-63046-5_23 |
| [12] | Lonsing, F.; Egly, U.; Seidl, M.; Creignou, N.; Le Berre, D., Q-resolution with generalized axioms, Theory and Applications of Satisfiability Testing - SAT 2016, 435-452 (2016), Cham: Springer, Cham · Zbl 1475.68442 · doi:10.1007/978-3-319-40970-2_27 |
| [13] | Plaisted, DA; Greenbaum, S., A structure-preserving clause form translation, J. Symb. Comput., 2, 3, 293-304 (1986) · Zbl 0636.68119 · doi:10.1016/S0747-7171(86)80028-1 |
| [14] | Rabe, M.N., Tentrup, L.: CAQE: a certifying QBF solver. In: FMCAD, pp. 136-143. IEEE (2015) |
| [15] | Reeves, JE; Heule, MJH; Bryant, RE, Moving definition variables in quantified Boolean formulas, Tools and Algorithms for the Construction and Analysis of Systems, 462-479 (2022), Cham: Springer, Cham · doi:10.1007/978-3-030-99524-9_26 |
| [16] | Tentrup, L.; Majumdar, R.; Kunčak, V., On expansion and resolution in CEGAR based QBF solving, Computer Aided Verification, 475-494 (2017), Cham: Springer, Cham · Zbl 1494.68293 · doi:10.1007/978-3-319-63390-9_25 |
| [17] | Tseitin, GS; Siekmann, JH; Wrightson, G., On the complexity of derivation in propositional calculus, Automation of Reasoning. Symbolic Computation, 466-483 (1983), Heidelberg: Springer, Heidelberg · doi:10.1007/978-3-642-81955-1_28 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
