Publications

See also the list of talks related to publications.

In reverse chronological ordering:

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 (TBA). Preprint (TBA).

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. Jarvisalo, F. Lonsing, M. Seidl, A. Biere: Clause Elimination for SAT and QSAT. J. Artif. Intell. Res. (JAIR) 53: 127-168 (2015).

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.

Home / Kontakt / Webmaster / Offenlegung gemäß § 25 Mediengesetz: Inhaber der Website ist die Fakultät für Informatik an der Technischen Universität Wien, 1040 Wien. Die TU Wien distanziert sich von den Inhalten aller extern gelinkten Seiten und übernimmt diesbezüglich keine Haftung. / Disclaimer. Datenschutzerklärung.