<div class="csl-bib-body">
<div class="csl-entry">Simader, M., Rebola-Pardo, A., & Seidl, M. (2025). FERAT: A New Expansion-Based Certification Framework for Quantified Boolean Formulas. In <i>SAC ’25: Proceedings of the 40th ACM/SIGAPP Symposium on Applied Computing</i> (pp. 1043–1050). https://doi.org/10.1145/3672608.3707863</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/225594
-
dc.description.abstract
To witness the correctness of unsatisfiablility results of SAT solvers, the powerful resolution asymmetric tautology (RAT) proof system has been introduced, for which efficient proof checkers are available. To harness the power of recent SAT technology for solving quantified Boolean formulas (QBFs), the extension of SAT with quantifiers over the Boolean variables, we introduce the proof system Exp+RAT. With this proof system, it becomes possible to use modern SAT solvers for expansion-based QBF solving, one of the most successful QBF solving paradigms. So far, expansion-based QBF solving relied on the resolution-based Exp+Res proof system which is less powerful than Exp+RAT.Based on the Exp+RAT proof system, we present the new certification framework FERAT for generating and checking Exp+RAT certificates. In a detailed evaluation, we show that with the FERAT pipeline, more formula instances can be certified than with the previous FERP pipeline which relies on the Exp+Res proof system.
en
dc.language.iso
en
-
dc.subject
certification
en
dc.subject
proof checking
en
dc.subject
quantified boolean formulas
en
dc.title
FERAT: A New Expansion-Based Certification Framework for Quantified Boolean Formulas
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.contributor.affiliation
Johannes Kepler University of Linz, Austria
-
dc.contributor.affiliation
Johannes Kepler University of Linz, Austria
-
dc.relation.isbn
979-8-4007-0629-5
-
dc.description.startpage
1043
-
dc.description.endpage
1050
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
SAC '25: Proceedings of the 40th ACM/SIGAPP Symposium on Applied Computing
-
tuw.peerreviewed
true
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publisher.doi
10.1145/3672608.3707863
-
dc.description.numberOfPages
8
-
tuw.author.orcid
0009-0002-5751-7820
-
tuw.author.orcid
0000-0001-9234-4377
-
tuw.author.orcid
0000-0002-3267-4494
-
tuw.event.name
40th ACM/SIGAPP Symposium on Applied Computing (SAC '25)
en
dc.description.sponsorshipexternal
Austrian Science Fund (FWF)
-
dc.description.sponsorshipexternal
State of Upper Austria
-
dc.relation.grantnoexternal
10.55776/COE12
-
dc.relation.grantnoexternal
LIT AI Lab
-
tuw.event.startdate
31-03-2025
-
tuw.event.enddate
04-04-2025
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Catania
-
tuw.event.country
IT
-
tuw.event.presenter
Simader, Marcel
-
tuw.event.track
Multi Track
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.grantfulltext
none
-
item.fulltext
no Fulltext
-
item.cerifentitytype
Publications
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.languageiso639-1
en
-
item.openairetype
conference paper
-
crisitem.author.dept
Johannes Kepler University of Linz, Austria
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering