Publications Andreas Fröhlich

2016

Andreas Fröhlich. Theoretical and Practical Aspects of Bit-Vector Reasoning. Dissertation Technische Wissenschaften, Informatik, Johannes Kepler University, Linz, 2016.
[ thesis | bibtex ]

2015

Aina Niemetz, Mathias Preiner, Armin Biere, Andreas Fröhlich. Improving Local Search For Bit-Vector Logics in SMT with Path Propagation. In Proc. 4th Intl. Work. on Design and Implementation of Formal Tools and Systems (DIFTS'15), 10 pages, aff. to FMCAD'15, Austin, TX, USA, 2015.

Armin Biere, Andreas Fröhlich. Evaluating CDCL Variable Scoring Schemes. In Proc. 18th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'15), Lecture Notes in Computer Science (LNCS) vol. 9340, 405-422, Springer 2015.

Armin Biere, Andreas Fröhlich. Evaluating CDCL Restart Schemes (preliminary version). In Proc. Intl. Workshop on Pragmatics of SAT (POS'15), 16 pages, aff. to SAT'15, Austing, TX, USA, 2015.

Gergely Kovásznai, Andreas Fröhlich, Armin Biere. Complexity of Fixed-Size Bit-Vector Logics (preprint). Theory of Computing Systems (TOCS), vol. 59, number 2, pages 323-376, Springer 2016, first online Sept. 2015.
[ preprint | bibtex ]

Andreas Fröhlich, Armin Biere, Christoph Wintersteiger, Youssef Hamadi. Stochastic Local Search for Satisfiability Modulo Theories. In Proc. 29th AAAI Conf. on Artificial Intelligence (AAAI'15), pages 1136 - 1143, AAAI Press 2015.

2014

Gergely Kovásznai, Helmut Veith, Andreas Fröhlich, Armin Biere. On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic. In Proc. 39th Intl. Symp. on Mathematical Foundations of Computer Science (MFCS'14), Lecture Notes in Computer Science (LNCS) vol. 8635, 481-492, Springer 2014.

Andreas Fröhlich, Gergely Kovásznai, Armin Biere, Helmut Veith. iDQ: Instantiation-Based DQBF Solving. In Proc. Intl. Workshop on Pragmatics of SAT (POS'14), EPiC Series, vol. 27, pages 103-116, EasyChair 2014.

Adrian Balint, Armin Biere, Andreas Fröhlich, Uwe Schöning. Improving implementation of SLS solvers for SAT and new heuristics for k-SAT with long clauses. In Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Lecture Notes in Computer Science (LNCS) vol. 8561, 302-316, Springer 2014.

Tomas Balyo, Andreas Fröhlich, Marijn Heule, Armin Biere. Everything You Always Wanted to Know About Blocked Sets (But Were Afraid to Ask). In Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Lecture Notes in Computer Science (LNCS) vol. 8561, 317-332, Springer 2014.

2013

Andreas Fröhlich, Gergely Kovásznai, Armin Biere. Efficiently Solving Bit-Vector Problems Using Model Checkers. In Proc. 11th Intl. Workshop on Satisfiability Modulo Theories (SMT'13), pages 6-15, aff. to SAT'13, Helsinki, Finland, 2013.

Gergely Kovásznai, Andreas Fröhlich, Armin Biere. Quantifier-Free Bit-Vector Formulas with Binary Encoding: Benchmark Description. In Proceedings of SAT Competition 2013, A. Balint, A. Belov, M. Heule, M. Järvisalo (editors), vol. B-2013-1 of Department of Computer Science Series of Publications B, pages 107 - 108 , University of Helsinki, 2013.

Gergely Kovásznai, Andreas Fröhlich, Armin Biere. BV2EPR: A Tool for Polynomially Translating Quantifier-free Bit-Vector Formulas into EPR. In Proc. 24th Intl. Conf.  on Automated Deduction (CADE'13), Lecture Notes in Computer Science (LNCS), pages 443-449, Springer 2013.

Andreas Fröhlich, Gergely Kovásznai, Armin Biere. More on the Complexity of Quantifier-Free Fixed-Size Bit-Vector Logics with Binary Encoding. In Proc. 8th Intl. Computer Science Symp. in Russia (CSR'13), Lecture Notes in Computer Science (LNCS), pages 378-390, Springer 2013 (with appendix).

2012

Gergely Kovásznai, Andreas Fröhlich, Armin Biere. On the Complexity of Fixed-Size Bit-Vector Logics with Binary Encoded Bit-Width. In Proc. 10th Intl. Workshop on Satisfiability Modulo Theories (SMT'12), pages 44-55, aff. to IJCAR'12, Manchester, UK, 2012.

Andreas Fröhlich, Gergely Kovásznai, Armin Biere. A DPLL Algorithm for Solving DQBF. In Proc. Intl. Workshop on Pragmatics of SAT (POS'12), aff. to SAT'12, Trento, Italy, 2012.

2010

Adrian Balint, Andreas Fröhlich. Improving stochastic local search for SAT with a new probability distribution In Proc. 13th Intl. Conference on Theory and Applications of Satisfiability Testing (SAT'10), Edinburgh, Scotland, UK, 2010