True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers

Description

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.

Period	05 Sept 2023
Event title	CICM 2023: 16TH CONFERENCE ON INTELLIGENT COMPUTER MATHEMATICS
Event type	Conference
Location	United KingdomShow on map