2023
-
H. Wu, C. Hahn, F. Lonsing, M. Mann, R. Ramanujan, C. W. Barrett:
Lightweight Online Learning for Sets of Related Problems in Automated Reasoning. In Proc. 23rd Conference on Formal Methods in
Computer-Aided Design
(FMCAD), 2023. Nomination for best paper award. Preprint
with appendix.
Proceedings version.
Source code.
-
S. Chattopadhyay, K. Devarajegowda, B. Zhao, F. Lonsing, B. D'Agostino, I. Vavelidou, V. Deep Bhatt, S. Prebeck, W. Ecker, C. Trippel, C. W. Barrett, S. Mitra:
G-QED: Generalized QED Pre-silicon Verification beyond Non-Interfering Hardware Accelerators.
In Proc. 60th ACM/IEEE Design Automation Conference
(DAC), 2023. Proceedings version.
2021
-
S. Chattopadhyay, F. Lonsing, L. Piccolboni, D. Soni, P. Wei,
X. Zhang, Y. Zhou, L. Carloni, D. Chen, J. Cong, R. Karri, Z. Zhang,
C. Trippel, C. Barrett, S. Mitra: Scaling Up Hardware Accelerator
Verification using A-QED with Functional
Decomposition. In Proc. 21st Conference on Formal Methods in
Computer-Aided Design
(FMCAD). IEEE,
2021. Preprint
with appendix.
Proceedings
version.
Software
artifact.
-
R. Bloem, N. Braud-Santoni, V. Hadzic, U. Egly, F. Lonsing, and
M. Seidl: Two
SAT solvers for solving quantified Boolean formulas with an
arbitrary number of quantifier
alternations. Formal
Methods in System Design, 2021.
-
M. Mann, A. Irfan, F. Lonsing, Y. Yang, H. Zhang, K. Brown, A. Gupta,
C. Barrett: Pono:
A Flexible and Extensible SMT-Based Model
Checker. In Proc. 33rd International Conference on
Computer Aided Verification
(CAV). LNCS, Springer,
2021. Source
code of related tool.
-
O. Beyersdorff, M. Janota, F. Lonsing, M. Seidl:
Quantified Boolean
Formulas. In Handbook
of Satisfiability. Second Edition. Editors: A. Biere,
M. Heule, H. van Maaren, T. Walsh. Volume 336 of Frontiers in
Artificial Intelligence and Applications. IOS Press. Preprint (PDF).
2020
-
F. Lonsing, S. Mitra, and C. Barrett: A Theoretical Framework for
Symbolic Quick Error Detection. In Proc. 20th Conference on Formal Methods in
Computer-Aided Design
(FMCAD). IEEE,
2020. Preprint with additional proofs (PDF).
Honorable Mention at FMCAD. Proceedings version.
-
E. Singh, F. Lonsing, S. Chattopadhyay, M. Strange, P. Wei, X. Zhang,
Y. Zhou, D. Chen, J. Cong, P. Raina, Z. Zhang, C. Barrett and
S. Mitra: A-QED Verification of Hardware
Accelerators. In Proc. 57th Design Automation Conference
(DAC). ACM, 2020. Preprint (PDF).
2019
-
F. Lonsing, K. Ganesan, M. Mann, S. Nuthakki, E. Singh, M. Srouji,
Y. Yang, S. Mitra, and C. Barrett: Unlocking the Power of Formal
Hardware Verification with CoSA and Symbolic QED. Invited
paper. In Proc. 2019 International Conference on Computer
Aided Design (ICCAD). IEEE,
2019. Preprint.
F. Lonsing: QBFRelay, QRATPre+, and DepQBF: Incremental Preprocessing Meets Search-Based QBF Solving. Journal
on Satisfiability, Boolean Modeling and Computation (JSAT), Volume
11 2019, pages 211-220, system description.
-
F. Lonsing and U. Egly: QRATPre+: Effective QBF Preprocessing via Strong Redundancy Properties. In Proc. 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT). LNCS, Springer, 2019. Preprint of
proceedings version with appendix, source code of related tool.
2018
- R. Bloem, N. Braud-Santoni, V. Hadzic, U. Egly, F. Lonsing, and M. Seidl: Expansion-Based QBF Solving Without Recursion. Proc. Formal Methods in
Computer-Aided Design (FMCAD),
2018. Proceedings
version. Preprint. (NOTE:
an extended journal version of this
article appeared in Formal Methods in System Design, Springer, 2021.)
-
F. Lonsing and U. Egly: Evaluating QBF Solvers: Quantifier Alternations
Matter. In Proc. 24th International Conference on Principles and
Practice of Constraint Programming
(CP). LNCS, Springer, 2018. Preprint of
proceedings version with appendix.
-
F. Lonsing and U. Egly: QRAT+: Generalizing QRAT by a More Powerful QBF Redundancy Property. In Proc. 9th International Joint
Conference on Automated Reasoning
(IJCAR), part of FLoC. LNCS,
Springer, 2018. Preprint of
proceedings version with appendix, source code of related tool.
-
F. Lonsing and M. Seidl: Parallel Solving of Quantified Boolean
Formulas. In Handbook of Parallel Constraint Reasoning, Springer
International Publishing, 2018.
2017
-
F. Lonsing and U. Egly: DepQBF 6.0: A Search-Based QBF Solver Beyond
Traditional QCDCL. In Proc. 26th International Conference on Automated
Deduction (CADE-26), LNCS,
Springer, 2017. Preprint of proceedings version with appendix
(PDF).
U. Egly, M. Kronegger, F. Lonsing, and A. Pfandler: Conformant Planning
as a Case Study of Incremental QBF Solving. Annals of Mathematics and
Artificial Intelligence, 80(1):21-45, Springer, 2017. Open access
article.
(NOTE: a preliminary version of this
article appeared in the proceedings of AISC 2014, LNCS, Springer.)
2016
-
F. Lonsing and M. Seidl, editors. Proceedings of the 4th International Workshop
on Quantified Boolean Formulas (QBF 2016), Bordeaux, France, July 4, 2016 co-located with
19th
Intl. Conf. on Theory and Applications of Satisfiability
Testing (SAT 2016),
volume 1719 of CEUR Workshop Proceedings. CEUR-WS.org, 2016.
-
F. Lonsing, U. Egly, and M. Seidl:
Q-Resolution with Generalized Axioms. In Proc. 19th
Intl. Conf. on Theory and Applications of Satisfiability
Testing (SAT 2016), LNCS,
Springer, 2016. Preprint of
proceedings version with appendix (PDF).
-
T. Balyo and F. Lonsing:
HordeQBF: A Modular and Massively Parallel QBF Solver. In Proc. 19th
Intl. Conf. on Theory and Applications of Satisfiability
Testing (SAT 2016), LNCS,
Springer, 2016. Preprint of
proceedings version (PDF).
-
F. Lonsing, M. Seidl, and A. Van Gelder:
The QBF Gallery:
Behind the Scenes. In Artificial Intelligence, 237:92-114, Elsevier, 2016. Preprint (PDF).
-
M. Janota, C. Jordan, W. Klieber, F. Lonsing, M. Seidl, A. Van
Gelder: The QBF Gallery 2014: The QBF Competition at the FLoC
Olympic Games. Journal on Satisfiability, Boolean Modeling and
Computation (JSAT), 9:187-206, 2016.
2015
-
F. Lonsing, F. Bacchus, A. Biere, U. Egly, and M. Seidl: Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination. In Proc. 20th International Conference on Logic for
Programming, Artificial Intelligence and Reasoning (LPAR 2015), LNCS,
Springer, 2015. Preprint of proceedings version (PDF).
-
U. Egly, F. Lonsing, and J. Oetsch: Automated Benchmarking of Incremental SAT and QBF Solvers. In Proc. 20th International Conference on Logic for
Programming, Artificial Intelligence and Reasoning (LPAR 2015), LNCS,
Springer, 2015. Preprint of proceedings version with
appendix (PDF).
-
F. Lonsing and U. Egly:
Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group
Solver API. In Proc. 18th
Intl. Conf. on Theory and Applications of Satisfiability
Testing (SAT 2015), LNCS,
Springer, 2015. Proceedings
version. Preprint of
proceedings version with appendix (PDF).
-
M. Heule, M. Järvisalo, F. Lonsing, M. Seidl, A. Biere:
Clause Elimination for SAT and QSAT. J. Artif. Intell. Res. (JAIR) 53: 127-168 (2015).
NOTE: winner of the 2019 IJCAI-JAIR Best Paper Prize.
2014
R. Bloem, U. Egly, P. Klampfl, R. Koenighofer and F. Lonsing. SAT-Based
Methods for Circuit Synthesis. Proc. Formal Methods in
Computer-Aided Design (FMCAD),
2014. Proceedings
version. Preprint with appendix.
F. Lonsing and U. Egly. Incremental QBF
Solving. In Proceedings of the 20th International Conference on Principles and Practice of
Constraint Programming, LNCS, Springer,
2014. Proceedings version.Preprint.
F. Lonsing and U. Egly. Incremental QBF
Solving by DepQBF. In Proc. 4th International Congress on
Mathematical Software (ICMS 2014), Lecture Notes in Computer
Science (LNCS) vol. 8592, pages 307-314, Springer
2014. Preprint.
U. Egly, M. Kronegger, F. Lonsing, and A. Pfandler: Conformant Planning
as a Case Study of Incremental QBF Solving. Proc. 12th
International Conference on Artificial Intelligence and Symbolic
Computation (AISC), volume 8884 of Lecture Notes in Artificial
Intelligence (LNAI), Springer,
2014. Preprint. (NOTE:
an extended journal version of this
article appeared in Annals of Mathematics and Artificial Intelligence,
Springer, 2017.)
C. Jordan, L. Kaiser, F. Lonsing, and M. Seidl. MPIDepQBF:
Towards
Parallel QBF Solving Without Knowledge Sharing. In Proc. 17th
Intl. Conf. on Theory and Applications of Satisfiability
Testing (SAT'14), Lecture Notes in Computer
Science (LNCS) vol. 8561, pages 430-437, Springer
2014.
2013
U. Egly, F. Lonsing, and M. Widl. Long-Distance Resolution: Proof Generation and Strategy
Extraction in Search-Based QBF Solving. In Proc. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2013), Lecture Notes in Computer
Science (LNCS) vol. 8312, pages 291-308, Springer
2013. Preprint.
F. Lonsing, U. Egly, and A. Van Gelder. Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation. In Proc. 16th
Intl. Conf. on Theory and Applications of Satisfiability
Testing (SAT'13), Lecture Notes in Computer
Science (LNCS) vol. 7962, pages 100-115, Springer
2013. Preprint: PDF.
2012
-
M. Seidl, F. Lonsing, A. Biere. QBF2EPR: A
Tool for Generating EPR Formulas from QBF In Proc. 3rd
Intl. Workshop. on Practical Aspects of Automated
Reasoning (PAAR'12), aff. to IJCAR'12, Manchester, UK,
2012.
A. Niemetz, M. Preiner, F. Lonsing, M. Seidl, and A. Biere. Resolution-Based Certificate Extraction for
QBF - (Tool Presentation). In Proc. 15th
Intl. Conf. on Theory and Applications of Satisfiability
Testing (SAT'12), Lecture Notes in Computer
Science (LNCS) vol. 7317, pages 430-435, Springer
2012.
A. Van Gelder, S. B. Wood, and F. Lonsing. Extended Failed-Literal Preprocessing for Quantified Boolean Formulas. In Proc. 15th
Intl. Conf. on Theory and Applications of Satisfiability
Testing (SAT'12), Lecture Notes in Computer
Science (LNCS) vol. 7317, pages 86-99, Springer
2012.
- Florian Lonsing. Dependency Schemes and Search-Based QBF Solving: Theory and
Practice. PhD Thesis. Johannes Kepler University, Linz, Austria. 2012
2011
A. Biere, F. Lonsing, and M. Seidl. Blocked Clause
Elimination for QBF. In Proc. 23rd
Intl. Conf. on Automated Deduction (CADE'11),
Lecture Notes in
Computer Science (LNCS) vol. 6803, pages 101-115, Springer
2011.
F. Lonsing, A. Biere. Failed Literal
Detection for QBF. In Proc. 14th
Intl. Conf. on Theory and Applications of Satisfiability
Testing (SAT'11), Lecture Notes in Computer
Science (LNCS) vol. 6695, pages 259-272, Springer
2011.
2010
F. Lonsing, A. Biere. Integrating
Dependency Schemes in Search-Based QBF Solvers. In
Proc. 13th Intl. Conf. on Theory and Applications
of Satisfiability Testing (SAT'10), Lecture Notes in Computer
Science (LNCS) vol. 6175, pages 158-171, Springer 2010.
(ERRATA).
R. Brummayer, F. Lonsing, A. Biere. Automated
Testing and Debugging of SAT and QBF Solvers. In
Proc. 13th Intl. Conf. on Theory and Applications
of Satisfiability Testing (SAT'10), Lecture Notes in Computer
Science (LNCS) vol. 6175, pages 44-57, Springer 2010.
F. Lonsing, A. Biere. DepQBF:
A Dependency-Aware QBF Solver (System Description). Journal
on Satisfiability, Boolean Modeling and Computation (JSAT), Volume
7 2010, system description, pages 71-76. A preliminary
version appeared in Proc. Pragmatics of SAT Workshop
(POS'10), 2010.
2009
F. Lonsing, A. Biere. A Compact
Representation for Syntactic Dependencies in QBFs. In
Proc. 12th Intl. Conf. on Theory and Applications
of Satisfiability Testing (SAT'09), Lecture Notes in Computer
Science (LNCS) vol. 5584, pages 398-411, Springer
2009.
2008
F. Lonsing, A. Biere. Efficiently Representing Existential
Dependency Sets for Expansion-based QBF Solvers. In Selected
Papers of Proc. 4th Doctoral Workshop on Mathematical and
Engineering Methods in Computer Science (MEMICS'08), Znojmo,
Czech Republic, November 2008. Appeared in ENTCS, vol. 251, pages
83 - 95, Elsevier 2009. (DOI) (Preprint)
(Preliminary
version)
R. Brummayer, A. Biere, F. Lonsing. BTOR:
Bit-Precise Modelling of Word-Level Problems for Model
Checking. In Proc. 1st Intl. Workshop on
Bit-Precise Reasoning (BPR'08), Princeton, New Jersey, USA,
July 2008.
- F. Lonsing, A. Biere. Nenofex:
Expanding NNF for QBF Solving. In Proc. 11th
Intl. Conf. on Theory and Applications of Satisfiability
Testing (SAT'08), Lecture Notes in Computer
Science (LNCS) vol. 4996, Springer 2008.
F. Lonsing An Expansion-based QBF Solver
for Negation Normal Form. Master Thesis, JKU Linz, 2008.