Armin Biere
56 publications
9 venues
H Index 25
Affiliation
Universit t Freiburg, GermanyJohannes Kepler University of Linz, Austria
Links
DBLPGoogle Scholar
ORCID- https://cca.informatik.uni-freiburg.de/biere/
- https://zbmath.org/authors/?q=ai:biere.armin
- https://mathgenealogy.org/id.php?id=111891
- https://www.wikidata.org/entity/Q687404
- https://www.researcherid.com/rid/C-4438-2013
- http://isni.org/isni/0000000078579332
- https://id.loc.gov/authorities/names/no2006075968
- https://d-nb.info/gnd/115751823
| Name | Venue | Year | citations |
|---|---|---|---|
MaxSAT Fuzzing and Delta Debugging.
|
JAIR | 2026 | 0 |
| Streamlining Distributed SAT Solver Design.
|
SAT | 2025 | 0 |
| Learn to Unlearn.
|
SAT | 2025 | 0 |
| Disjoint projected enumeration for SAT and SMT without blocking clauses.
|
Artificial Intelligence | 2025 | 0 |
| Dynamic Blocked Clause Elimination for Projected Model Counting.
|
SAT | 2024 | 2 |
| Clausal Congruence Closure.
|
SAT | 2024 | 5 |
| Satisfiability Modulo User Propagators.
|
JAIR | 2024 | 7 |
| Certifying Incremental SAT Solving.
|
LPAR | 2024 | 6 |
| Improved Bounds of Integer Solution Counts via Volume and Extending to Mixed-Integer Linear Constraints.
|
CP | 2024 | 1 |
| Disjoint Partial Enumeration without Blocking Clauses.
|
AAAI | 2024 | 0 |
| CadiBack: Extracting Backbones with CaDiCaL.
|
SAT | 2023 | 9 |
| IPASIR-UP: User Propagators for CDCL.
|
SAT | 2023 | 24 |
| Faster LRAT Checking Than Solving with CaDiCaL.
|
SAT | 2023 | 13 |
| Better Decision Heuristics in CDCL through Local Search and Target Phases.
|
JAIR | 2022 | 24 |
| Migrating Solver State.
|
SAT | 2022 | 3 |
| Non-clausal Redundancy Properties.
|
CADE | 2021 | 5 |
| Efficient All-UIP Learned Clause Minimization.
|
SAT | 2021 | 6 |
| XOR Local Search for Boolean Brent Equations.
|
SAT | 2021 | 3 |
| Decomposition Strategies to Count Integer Solutions over Linear Constraints.
|
IJCAI | 2021 | 8 |
| Four Flavors of Entailment.
|
SAT | 2020 | 9 |
| Duplex Encoding of Staircase At-Most-One Constraints for the Antibandwidth Problem.
|
CPAIOR | 2020 | 6 |
| Distributed Cube and Conquer with Paracooba.
|
SAT | 2020 | 20 |
| Backing Backtracking.
|
SAT | 2019 | 26 |
| Incremental Inprocessing in SAT Solving.
|
SAT | 2019 | 41 |
| Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood?
|
IJCAI | 2017 | 3 |
| Blocked Clauses in First-Order Logic.
|
LPAR | 2017 | 15 |
| Short Proofs Without New Variables.
|
CADE | 2017 | 43 |
| SAT Race 2015.
|
Artificial Intelligence | 2016 | 65 |
| Evaluating CDCL Variable Scoring Schemes.
|
SAT | 2015 | 98 |
| Clause Elimination for SAT and QSAT.
|
JAIR | 2015 | 76 |
| Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination.
|
LPAR | 2015 | 34 |
| Compositional Propositional Proofs.
|
LPAR | 2015 | 14 |
| Stochastic Local Search for Satisfiability Modulo Theories.
|
AAAI | 2015 | 44 |
| Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses.
|
SAT | 2014 | 19 |
| Detecting Cardinality Constraints in CNF.
|
SAT | 2014 | 49 |
| Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask).
|
SAT | 2014 | 18 |
| Revisiting Hyper Binary Resolution.
|
CPAIOR | 2013 | 26 |
| Factoring Out Assumptions to Speed Up MUS Extraction.
|
SAT | 2013 | 47 |
| : A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into.
|
CADE | 2013 | 3 |
| Blocked Clause Decomposition.
|
LPAR | 2013 | 25 |
| Resolution-Based Certificate Extraction for QBF - (Tool Presentation).
|
SAT | 2012 | 65 |
| Concurrent Cube-and-Conquer - (Poster Presentation).
|
SAT | 2012 | 9 |
| Efficient CNF Simplification Based on Binary Implication Graphs.
|
SAT | 2011 | 68 |
| Failed Literal Detection for QBF.
|
SAT | 2011 | 21 |
| Blocked Clause Elimination for QBF.
|
CADE | 2011 | 127 |
| Automated Testing and Debugging of SAT and QBF Solvers.
|
SAT | 2010 | 113 |
| Integrating Dependency Schemes in Search-Based QBF Solvers.
|
SAT | 2010 | 57 |
| Reconstructing Solutions after Blocked Clause Elimination.
|
SAT | 2010 | 25 |
| Minimizing Learned Clauses.
|
SAT | 2009 | 119 |
| A Compact Representation for Syntactic Dependencies in QBFs.
|
SAT | 2009 | 17 |
| Nenofex: Expanding NNF for QBF Solving.
|
SAT | 2008 | 51 |
| Adaptive Restart Strategies for Conflict Driven SAT Solvers.
|
SAT | 2008 | 118 |
| A First Step Towards a Unified Proof Checker for QBF.
|
SAT | 2007 | 54 |
| Extended Resolution Proofs for Symbolic SAT Solving with Quantification.
|
SAT | 2006 | 49 |
| Effective Preprocessing in SAT Through Variable and Clause Elimination.
|
SAT | 2005 | 741 |
| Resolve and Expand.
|
SAT | 2004 | 296 |