True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers

Simone Heisinger; Martina Seidl

doi:10.1007/978-3-031-42753-4_20

True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

Abstract

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.

Original language	English
Title of host publication	Intelligent Computer Mathematics. CICM 2023
Editors	Catherine Dubois, Manfred Kerber
Publisher	Springer
Pages	291–296
Number of pages	6
Volume	14101
ISBN (Print)	978-3-031-42752-7
DOIs	https://doi.org/10.1007/978-3-031-42753-4_20
Publication status	Published - Aug 2023

Publication series

Name	Lecture Notes in Computer Science (LNCS)

Fields of science

101013 Mathematical logic
102 Computer Sciences
102001 Artificial intelligence
102011 Formal languages
102022 Software development
102030 Semantic technologies
102031 Theoretical computer science
603109 Logic

JKU Focus areas

Digital Transformation

Access to Document

10.1007/978-3-031-42753-4_20

Cite this

@inproceedings{557a0de99d7248208a25f8e71cb1b30d,

title = "True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers",

abstract = "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.",

author = "Simone Heisinger and Martina Seidl",

year = "2023",

month = aug,

doi = "10.1007/978-3-031-42753-4_20",

language = "English",

isbn = "978-3-031-42752-7",

volume = "14101",

series = "Lecture Notes in Computer Science (LNCS)",

publisher = "Springer",

pages = "291–296",

editor = "{Catherine Dubois, Manfred Kerber}",

booktitle = "Intelligent Computer Mathematics. CICM 2023",

}

True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers. / Heisinger, Simone ; Seidl, Martina.
Intelligent Computer Mathematics. CICM 2023. ed. / Catherine Dubois, Manfred Kerber. Vol. 14101 Springer, 2023. p. 291–296 (Lecture Notes in Computer Science (LNCS)).

Research output: Chapter in Book/Report/Conference proceeding › Conference proceedings › peer-review

TY - GEN

T1 - True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers

AU - Heisinger, Simone

AU - Seidl, Martina

PY - 2023/8

Y1 - 2023/8

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-031-42753-4_20

DO - 10.1007/978-3-031-42753-4_20

M3 - Conference proceedings

SN - 978-3-031-42752-7

VL - 14101

T3 - Lecture Notes in Computer Science (LNCS)

SP - 291

EP - 296

BT - Intelligent Computer Mathematics. CICM 2023

A2 - Catherine Dubois, Manfred Kerber, null

PB - Springer

ER -