<div class="csl-bib-body">
<div class="csl-entry">Adame, B. O., Bogaerts, B., Bogø, B., Dold, S., GONTIER, A., Koops, W., McCreesh, C., McIlree, M., Nordström, J., Oertel, A., Rebola Pardo, A., & Turnbull, M. P. (2026). Trimming Pseudo-Boolean Proofs. In B. Dutertre & B. Könighofer (Eds.), <i>Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026</i> (pp. 743–756). TU Wien Academic Press. https://doi.org/10.34727/2026/isbn.978-3-85448-093-8_74</div>
</div>
Modern combinatorial solvers are very efficient but also highly complex and therefore error-prone. The most successful approach to ensure correctness—proof logging—is now the accepted standard for Boolean satisfiability (SAT) solving, where proof trimming is an additional crucial technique to reduce proof size and proof checking time. However, efficient proof logging has remained a challenge for richer combinatorial paradigms, and trimming has not been supported for the more complex proof logging systems used. In this work, we present a proof trimmer covering the full VERIPB proof format, bringing the advantages of trimming to a wide range of paradigms such as MaxSAT,
en
dc.language.iso
en
-
dc.rights.uri
http://creativecommons.org/licenses/by/4.0/
-
dc.subject
formal methods
en
dc.subject
computer-aided system design
en
dc.subject
hardware and system verification
en
dc.title
Trimming Pseudo-Boolean Proofs
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.rights.license
Creative Commons Namensnennung 4.0 International
de
dc.rights.license
Creative Commons Attribution 4.0 International
en
dc.identifier.doi
10.34727/2026/isbn.978-3-85448-093-8_74
-
dc.contributor.affiliation
Electrical and Computer Engineering - Arba Minch University (Arba Minch, ET)
-
dc.contributor.affiliation
Vrije Universiteit Brussel (Brussels, BE)
-
dc.contributor.affiliation
University of Basel (Basel, CH)
-
dc.contributor.affiliation
School of Computing Science - University of Glasgow (Glasgow, GB)
-
dc.contributor.affiliation
Lund University (Lund, SE)
-
dc.contributor.affiliation
University of Glasgow (Glasgow, GB)
-
dc.contributor.affiliation
Department of Computer Science - Lund University (Lund, SE)
-
dc.contributor.affiliation
-2026: Lund University (Lund, SE)
-
dc.contributor.affiliation
Data Access - SAS (Cary, US)
-
dc.contributor.editoraffiliation
Amazon Web Services
-
dc.contributor.editoraffiliation
Graz University of Technology (Graz, AT)
-
dc.relation.isbn
978-3-85448-093-8
-
dc.description.volume
7
-
dc.description.startpage
743
-
dc.description.endpage
756
-
dc.rights.holder
Berhan Oumer Adame, Bart Bogaerts, Benjamin Bogø, Simon Dold, Arthur Gontier, Wietze Koops, Ciaran McCreesh, Matthew McIlree, Jakob Nordström, Andy Oertel, Adrian Rebola-Pardo, and Mark Turnbull
-
dc.type.category
Full-Paper Contribution
-
dc.relation.eissn
2708-7824
-
tuw.booktitle
Proceedings of the 26th Conference on Formal Methods in Computer-Aided Design – FMCAD 2026
-
tuw.peerreviewed
true
-
tuw.relation.ispartof
10.34727/2026/isbn.978-3-85448-093-8
-
tuw.relation.publisher
TU Wien Academic Press
-
tuw.book.chapter
74
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.id
I2
-
tuw.researchTopic.id
C5
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.name
Computer Engineering and Software-Intensive Systems
-
tuw.researchTopic.name
Computer Science Foundations
-
tuw.researchTopic.value
40
-
tuw.researchTopic.value
40
-
tuw.researchTopic.value
20
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
dc.identifier.libraryid
AC18000698
-
dc.description.numberOfPages
14
-
tuw.relation.ispartoftuwseries
Conference Series: Formal Methods in Computer-Aided Design
-
tuw.author.orcid
0000-0003-4685-3781
-
tuw.author.orcid
0000-0003-3460-4251
-
tuw.author.orcid
0009-0000-2192-3291
-
tuw.author.orcid
0009-0003-6265-9484
-
tuw.author.orcid
0000-0002-9579-5584
-
tuw.author.orcid
0000-0001-9945-1992
-
tuw.author.orcid
0000-0002-6106-4871
-
tuw.author.orcid
0009-0005-5042-0876
-
tuw.author.orcid
0000-0002-2700-4285
-
tuw.author.orcid
0000-0001-9783-6768
-
tuw.author.orcid
0000-0001-9234-4377
-
tuw.author.orcid
0009-0000-7155-9176
-
dc.contributor.serieseditor
Hunt, Warren A., Jr.
-
dc.contributor.serieseditor
Weissenbacher, Georg
-
dc.rights.identifier
CC BY 4.0
de
dc.rights.identifier
CC BY 4.0
en
tuw.editor.orcid
0000-0002-6284-380X
-
tuw.editor.orcid
0000-0001-5183-5452
-
wb.sciencebranch
Informatik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.value
100
-
item.openaccessfulltext
Open Access
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.openairetype
conference paper
-
item.fulltext
with Fulltext
-
item.mimetype
application/pdf
-
item.grantfulltext
open
-
crisitem.author.dept
Electrical and Computer Engineering - Arba Minch University (Arba Minch, ET)
-
crisitem.author.dept
Vrije Universiteit Brussel (Brussels, BE)
-
crisitem.author.dept
University of Basel (Basel, CH)
-
crisitem.author.dept
School of Computing Science - University of Glasgow (Glasgow, GB)
-
crisitem.author.dept
Lund University (Lund, SE)
-
crisitem.author.dept
University of Glasgow (Glasgow, GB)
-
crisitem.author.dept
Department of Computer Science - Lund University (Lund, SE)
-
crisitem.author.dept
-2026: Lund University (Lund, SE)
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
