Armin Biere

51 publications

9 venues

H Index 22

Affiliation

Universit t Freiburg, Germany
Johannes Kepler University of Linz, Austria

Links

Name	Venue	Year	citations
Disjoint Partial Enumeration without Blocking Clauses.	AAAI	2024	0
Improved Bounds of Integer Solution Counts via Volume and Extending to Mixed-Integer Linear Constraints.	CP	2024	0
Dynamic Blocked Clause Elimination for Projected Model Counting.	SAT	2024	0
Clausal Congruence Closure.	SAT	2024	0
Certifying Incremental SAT Solving.	LPAR	2024	0
CadiBack: Extracting Backbones with CaDiCaL.	SAT	2023	0
Faster LRAT Checking Than Solving with CaDiCaL.	SAT	2023	0
IPASIR-UP: User Propagators for CDCL.	SAT	2023	0
Migrating Solver State.	SAT	2022	0
Better Decision Heuristics in CDCL through Local Search and Target Phases.	JAIR	2022	2
Efficient All-UIP Learned Clause Minimization.	SAT	2021	3
Non-clausal Redundancy Properties.	CADE	2021	3
XOR Local Search for Boolean Brent Equations.	SAT	2021	0
Decomposition Strategies to Count Integer Solutions over Linear Constraints.	IJCAI	2021	0
Four Flavors of Entailment.	SAT	2020	2
Duplex Encoding of Staircase At-Most-One Constraints for the Antibandwidth Problem.	CPAIOR	2020	2
Distributed Cube and Conquer with Paracooba.	SAT	2020	11
Incremental Inprocessing in SAT Solving.	SAT	2019	26
Backing Backtracking.	SAT	2019	18
Blocked Clauses in First-Order Logic.	LPAR	2017	12
Short Proofs Without New Variables.	CADE	2017	32
Blockedness in Propositional Logic: Are You Satisfied With Your Neighborhood?	IJCAI	2017	3
SAT Race 2015.	Artificial Intelligence	2016	52
Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination.	LPAR	2015	34
Clause Elimination for SAT and QSAT.	JAIR	2015	63
Compositional Propositional Proofs.	LPAR	2015	11
Stochastic Local Search for Satisfiability Modulo Theories.	AAAI	2015	34
Evaluating CDCL Variable Scoring Schemes.	SAT	2015	78
Everything You Always Wanted to Know about Blocked Sets (But Were Afraid to Ask).	SAT	2014	14
Detecting Cardinality Constraints in CNF.	SAT	2014	45
Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses.	SAT	2014	15
Blocked Clause Decomposition.	LPAR	2013	19
: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into.	CADE	2013	4
Factoring Out Assumptions to Speed Up MUS Extraction.	SAT	2013	45
Revisiting Hyper Binary Resolution.	CPAIOR	2013	19
Concurrent Cube-and-Conquer - (Poster Presentation).	SAT	2012	7
Resolution-Based Certificate Extraction for QBF - (Tool Presentation).	SAT	2012	56
Failed Literal Detection for QBF.	SAT	2011	21
Efficient CNF Simplification Based on Binary Implication Graphs.	SAT	2011	65
Blocked Clause Elimination for QBF.	CADE	2011	122
Reconstructing Solutions after Blocked Clause Elimination.	SAT	2010	23
Automated Testing and Debugging of SAT and QBF Solvers.	SAT	2010	93
Integrating Dependency Schemes in Search-Based QBF Solvers.	SAT	2010	57
A Compact Representation for Syntactic Dependencies in QBFs.	SAT	2009	18
Minimizing Learned Clauses.	SAT	2009	117
Nenofex: Expanding NNF for QBF Solving.	SAT	2008	50
Adaptive Restart Strategies for Conflict Driven SAT Solvers.	SAT	2008	112
A First Step Towards a Unified Proof Checker for QBF.	SAT	2007	55
Extended Resolution Proofs for Symbolic SAT Solving with Quantification.	SAT	2006	41
Effective Preprocessing in SAT Through Variable and Clause Elimination.	SAT	2005	701
Resolve and Expand.	SAT	2004	294