Solution Counts of Some Prominent Quantified Boolean Formulas Families

Andreas Plank; Manuel Kauers; Martina Seidl

doi:10.1145/3672608.3707850

Solution Counts of Some Prominent Quantified Boolean Formulas Families

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

Abstract

Over the last years many problems from different application fields, like artificial intelligence, game theory and formal verification, have been solved by encoding them to quantified Boolean formulas (QBFs)[5]. Consequently, much progress has been made on solving techniques as well as on development of theory, partly based on generalizing known techniques from SAT (eg Q-resolution), partly being developed especially for QBFs (eg prenexing strategies). QBFs extend propositional formulas with existential and universal

Original language	English
Title of host publication	Proceedings of ACM SAC Conference (SAC’25)
Place of Publication	New York
Pages	1035-1042
Number of pages	8
ISBN (Electronic)	9798400706295
DOIs	https://doi.org/10.1145/3672608.3707850
Publication status	Published - 14 May 2025
Event	ACM SAC Conference 2025 - University of Catania, Catania, Italy Duration: 31 Mar 2025 → 04 Apr 2025 Conference number: 40 https://www.sigapp.org/sac/sac2025/index.php

Publication series

Name	Proceedings of the ACM Symposium on Applied Computing

Conference

Conference	ACM SAC Conference 2025
Abbreviated title	SAC 2025
Country/Territory	Italy
City	Catania
Period	31.03.2025 → 04.04.2025
Internet address	https://www.sigapp.org/sac/sac2025/index.php

Fields of science

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

JKU Focus areas

Digital Transformation

Access to Document

10.1145/3672608.3707850Licence: Other

Cite this

@inproceedings{5489222ca9b74da59d8d005ed3e590e3,

title = "Solution Counts of Some Prominent Quantified Boolean Formulas Families",

abstract = "Over the last years many problems from different application fields, like artificial intelligence, game theory and formal verification, have been solved by encoding them to quantified Boolean formulas (QBFs)[5]. Consequently, much progress has been made on solving techniques as well as on development of theory, partly based on generalizing known techniques from SAT (eg Q-resolution), partly being developed especially for QBFs (eg prenexing strategies). QBFs extend propositional formulas with existential and universal",

author = "Andreas Plank and Manuel Kauers and Martina Seidl",

year = "2025",

month = may,

day = "14",

doi = "10.1145/3672608.3707850",

language = "English",

series = "Proceedings of the ACM Symposium on Applied Computing",

pages = "1035--1042",

booktitle = "Proceedings of ACM SAC Conference (SAC{\textquoteright}25)",

note = "ACM SAC Conference 2025 ; Conference date: 31-03-2025 Through 04-04-2025",

url = "https://www.sigapp.org/sac/sac2025/index.php",

}

TY - GEN

T1 - Solution Counts of Some Prominent Quantified Boolean Formulas Families

AU - Plank, Andreas

AU - Kauers, Manuel

AU - Seidl, Martina

N1 - Conference code: 40

PY - 2025/5/14

Y1 - 2025/5/14

N2 - Over the last years many problems from different application fields, like artificial intelligence, game theory and formal verification, have been solved by encoding them to quantified Boolean formulas (QBFs)[5]. Consequently, much progress has been made on solving techniques as well as on development of theory, partly based on generalizing known techniques from SAT (eg Q-resolution), partly being developed especially for QBFs (eg prenexing strategies). QBFs extend propositional formulas with existential and universal

AB - Over the last years many problems from different application fields, like artificial intelligence, game theory and formal verification, have been solved by encoding them to quantified Boolean formulas (QBFs)[5]. Consequently, much progress has been made on solving techniques as well as on development of theory, partly based on generalizing known techniques from SAT (eg Q-resolution), partly being developed especially for QBFs (eg prenexing strategies). QBFs extend propositional formulas with existential and universal

UR - https://www.scopus.com/pages/publications/105006423211

U2 - 10.1145/3672608.3707850

DO - 10.1145/3672608.3707850

M3 - Conference proceedings

T3 - Proceedings of the ACM Symposium on Applied Computing

SP - 1035

EP - 1042

BT - Proceedings of ACM SAC Conference (SAC’25)

CY - New York

T2 - ACM SAC Conference 2025

Y2 - 31 March 2025 through 4 April 2025

ER -

Solution Counts of Some Prominent Quantified Boolean Formulas Families

Abstract

Publication series

Conference

Fields of science

JKU Focus areas

Access to Document

Other files and links

Cluster of Excellence "Bilateral Artificial Intelligence"

Constructive Decomposition of Matrix Multiplication Tensors

Algorithms for D-Algebraic Functions