Andreas Fröhlich

dblp:20/8296 · DBLP profile ↗
← Back
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
YearPublicationVenuePosition
2022 Keep It Simple: Local Search-based Latent Space Editing
Andreas Meißner, Andreas Fröhlich, Michaela Geierhos
IJCCI2
2021 XOR Local Search for Boolean Brent Equations
Wojciech Nawrocki, Zhenjun Liu, Andreas Fröhlich, Marijn Heule, Armin Biere
SAT3
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 Theories
abstract
Satisfiability 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
AAAI1
2015 Evaluating CDCL Variable Scoring Schemes
Armin Biere, Andreas Fröhlich
SAT2
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
SAT3
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
SAT2
2013 : A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into
Gergely Kovásznai, Andreas Fröhlich, Armin Biere
CADE2
2010 Improving Stochastic Local Search for SAT with a New Probability Distribution
Adrian Balint, Andreas Fröhlich
SAT2