VLDB 2026 Research / reviewers in the wild / expert
Andreas Fröhlich
dblp:20/8296
· DBLP profile ↗
10ranked-venue papers
1as first author
2since 2021 · last 2022
0000-0002-0698-3621ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Artificial intelligence and machine learning · 8 · 1 first-author · 2 since 2021Theory of computation · 8 · 1 since 2021Graphics, computer vision, multimedia, augmented reality and games · 1 · 1 first-author
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2022 | Keep It Simple: Local Search-based Latent Space Editing
Andreas Meißner, Andreas Fröhlich, Michaela Geierhos |
IJCCI | 2 |
| 2021 | XOR Local Search for Boolean Brent Equations
Wojciech Nawrocki, Zhenjun Liu, Andreas Fröhlich, Marijn Heule, Armin Biere |
SAT | 3 |
| 2016 | Complexity of Fixed-Size Bit-Vector Logics
Gergely Kovásznai, Andreas Fröhlich, Armin Biere |
Theory Comput. Syst. | 2 |
| 2015 | Stochastic Local Search for Satisfiability Modulo TheoriesabstractSatisfiability Modulo Theories (SMT) is essential for many practical applications, e.g., in hard- and software verification, and increasingly also in other scientific areas like computational biology. A large number of applications in these areas benefit from bit-precise reasoning over finite-domain variables. Current approaches in this area translate a formula over bit-vectors to an equisatisfiable propositional formula, which is then given to a SAT solver. In this paper, we present a novel stochastic local search (SLS) algorithm to solve SMT problems, especially those in the theory of bit-vectors, directly on the theory level. We explain how several successful techniques used in modern SLS solvers for SAT can be lifted to the SMT level. Experimental results show that our approach can compete with state-of-the-art bit-vector solvers on many practical instances and, sometimes, outperform existing solvers. This offers interesting possibilities in combining our approach with existing techniques, and, moreover, new insights into the importance of exploiting problem structure in SLS solvers for SAT. Our approach is modular and, therefore, extensible to support other theories, potentially allowing SLS to become part of the more general SMT framework. Andreas Fröhlich, Armin Biere, Christoph M. Wintersteiger, Youssef Hamadi |
AAAI | 1 |
| 2015 | Evaluating CDCL Variable Scoring Schemes
Armin Biere, Andreas Fröhlich |
SAT | 2 |
| 2014 | On the Complexity of Symbolic Verification and Decision Problems in Bit-Vector Logic
Gergely Kovásznai, Helmut Veith, Andreas Fröhlich, Armin Biere |
MFCS (2) | 3 |
| 2014 | Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses
Adrian Balint, Armin Biere, Andreas Fröhlich, Uwe Schöning |
SAT | 3 |
| 2014 | Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask)
Tomás Balyo, Andreas Fröhlich, Marijn Heule, Armin Biere |
SAT | 2 |
| 2013 | : A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into
Gergely Kovásznai, Andreas Fröhlich, Armin Biere |
CADE | 2 |
| 2010 | Improving Stochastic Local Search for SAT with a New Probability Distribution
Adrian Balint, Andreas Fröhlich |
SAT | 2 |