×

zbMATH — the first resource for mathematics

Biere, Armin

Compute Distance To:
Author ID: biere.armin Recent zbMATH articles by "Biere, Armin"
Published as: Biere, A.; Biere, Armin
External Links: MGP · ORCID · dblp
Documents Indexed: 86 Publications since 1999, including 12 Books

Publications by Year

Citations contained in zbMATH

60 Publications have been cited 677 times in 382 Documents Cited by Year
Handbook of satisfiability. Zbl 1183.68568
Biere, Armin (ed.); Heule, Marijn (ed.); van Maaren, Hans (ed.); Walsh, Toby (ed.)
133
2009
Effective preprocessing in SAT through variable and clause elimination. Zbl 1128.68463
Eén, Niklas; Biere, Armin
72
2005
Bounded model checking using satisfiability solving. Zbl 0985.68038
Clarke, Edmund; Biere, Armin; Raimi, Richard; Zhu, Yunshan
46
2001
PicoSAT essentials. Zbl 1159.68403
Biere, Armin
40
2008
Resolve and expand. Zbl 1122.68585
Biere, Armin
29
2005
Verifying safety properties of a PowerPC\(^{TM}\) microprocessor using symbolic model checking without BDDs. Zbl 1046.68578
Biere, Armin; Clarke, Edmund; Raimi, Richard; Zhu, Yunshan
28
1999
Inprocessing rules. Zbl 1358.68256
Järvisalo, Matti; Heule, Marijn J. H.; Biere, Armin
26
2012
Blocked clause elimination. Zbl 1284.03208
Järvisalo, Matti; Biere, Armin; Heule, Marijn
25
2010
Blocked clause elimination for QBF. Zbl 1341.68181
Biere, Armin; Lonsing, Florian; Seidl, Martina
18
2011
Clause elimination procedures for CNF formulas. Zbl 1306.68144
Heule, Marijn; Järvisalo, Matti; Biere, Armin
14
2010
Linear encodings of bounded LTL model checking. Zbl 1127.68057
Biere, Armin; Heljanko, Keijo; Junttila, Tommi; Latvala, Timo; Schuppan, Viktor
14
2006
A unified proof system for QBF preprocessing. Zbl 1409.68257
Heule, Marijn J. H.; Seidl, Martina; Biere, Armin
12
2014
Simulating circuit-level simplifications on CNF. Zbl 1267.94144
Järvisalo, Matti; Biere, Armin; Heule, Marijn J. H.
12
2012
Enhancing search-based QBF solving by dynamic blocked clause elimination. Zbl 06528797
Lonsing, Florian; Bacchus, Fahiem; Biere, Armin; Egly, Uwe; Seidl, Martina
11
2015
Clause elimination for SAT and QSAT. Zbl 1336.68231
Heule, Marijn; Järvisalo, Matti; Lonsing, Florian; Seidl, Martina; Biere, Armin
11
2015
Efficient CNF simplification based on binary implication graphs. Zbl 1330.68269
Heule, Marijn J. H.; Järvisalo, Matti; Biere, Armin
11
2011
Automated testing and debugging of SAT and QBF solvers. Zbl 1306.68155
Brummayer, Robert; Lonsing, Florian; Biere, Armin
11
2010
Integrating dependency schemes in search-based QBF solvers. Zbl 1306.68165
Lonsing, Florian; Biere, Armin
10
2010
Nenofex: Expanding NNF for QBF solving. Zbl 1138.68546
Lonsing, Florian; Biere, Armin
10
2008
Extended resolution proofs for conjoining BDDs. Zbl 1185.68635
Sinz, Carsten; Biere, Armin
9
2006
Adaptive restart strategies for conflict driven SAT solvers. Zbl 1138.68533
Biere, Armin
8
2008
A first step towards a unified proof checker for QBF. Zbl 1214.68334
Jussila, Toni; Biere, Armin; Sinz, Carsten; Kröning, Daniel; Wintersteiger, Christoph M.
8
2007
Lemmas on demand for the extensional theory of arrays. Zbl 1187.68168
Brummayer, Robert; Biere, Armin
7
2009
Compressing BMC encodings with QBF. Zbl 1277.68136
Jussila, Toni; Biere, Armin
7
2007
Liveness checking as safety checking for infinite state spaces. Zbl 1273.68240
Schuppan, Viktor; Biere, Armin
7
2006
Factoring out assumptions to speed up MUS extraction. Zbl 1390.68601
Lagniez, Jean-Marie; Biere, Armin
6
2013
Extended resolution proofs for symbolic SAT solving with quantification. Zbl 1187.68550
Jussila, Toni; Sinz, Carsten; Biere, Armin
6
2006
Super-blocked clauses. Zbl 06623253
Kiesl, Benjamin; Seidl, Martina; Tompits, Hans; Biere, Armin
5
2016
Blocked clause decomposition. Zbl 1407.68451
Heule, Marijn J. H.; Biere, Armin
5
2013
More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding. Zbl 1345.68172
Fröhlich, Andreas; Kovásznai, Gergely; Biere, Armin
5
2013
Failed literal detection for QBF. Zbl 1330.68118
Lonsing, Florian; Biere, Armin
5
2011
Combining decision diagrams and SAT procedures for efficient symbolic model checking. Zbl 0974.68526
Williams, Poul F.; Biere, Armin; Clarke, Edmund M.; Gupta, Anubhav
5
2000
SAT-based model checking. Zbl 1392.68232
Biere, Armin; Kröning, Daniel
4
2018
Complexity of fixed-size bit-vector logics. Zbl 1357.68086
Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin
4
2016
Shortest counterexamples for symbolic model checking of LTL with past. Zbl 1087.68060
Schuppan, Viktor; Biere, Armin
4
2005
Simple bounded LTL model checking. Zbl 1117.68432
Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi
4
2004
A satisfiability procedure for quantified Boolean formulae. Zbl 1029.68082
Plaisted, David A.; Biere, Armin; Zhu, Yunshan
4
2003
What a difference a variable makes. Zbl 1423.68419
Heule, Marijn J. H.; Biere, Armin
3
2018
Short proofs without new variables. Zbl 06778401
Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin
3
2017
Everything you always wanted to know about blocked sets (but were afraid to ask). Zbl 1423.68435
Balyo, Tomáš; Fröhlich, Andreas; Heule, Marijn J. H.; Biere, Armin
3
2014
Reconstructing solutions after blocked clause elimination. Zbl 1306.68159
Järvisalo, Matti; Biere, Armin
3
2010
Efficiently representing existential dependency sets for expansion-based QBF solvers. Zbl 1291.68358
Lonsing, Florian; Biere, Armin
3
2009
Blocked clauses in first-order logic. Zbl 1403.68240
Kiesl, Benjamin; Suda, Martin; Seidl, Martina; Tompits, Hans; Biere, Armin
2
2017
Propagation based local search for bit-precise reasoning. Zbl 1377.68134
Niemetz, Aina; Preiner, Mathias; Biere, Armin
2
2017
SAT race 2015. Zbl 1392.68381
Balyo, Tomáš; Biere, Armin; Iser, Markus; Sinz, Carsten
2
2016
Compositional propositional proofs. Zbl 06528799
Heule, Marijn J. H.; Biere, Armin
2
2015
Detecting cardinality constraints in CNF. Zbl 1423.68437
Biere, Armin; Le Berre, Daniel; Lonca, Emmanuel; Manthey, Norbert
2
2014
Tutorial on model checking: Modelling and verification in computer science. Zbl 1171.68546
Biere, Armin
2
2008
Theory and applications of satisfiability testing – SAT 2006. 9th international conference, Seattle, WA, USA, August 12–15, 2006. Proceedings. Zbl 1114.68003
Biere, Armin (ed.); Gomes, Carla P. (ed.)
2
2006
Decomposing SAT problems into connected components. Zbl 1116.68079
Biere, Armin; Sinz, Carsten
2
2006
Strong extension-free proof systems. Zbl 07176609
Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin
1
2020
Incremental inprocessing in SAT solving. Zbl 1441.68224
Fazekas, Katalin; Biere, Armin; Scholl, Christoph
1
2019
Solution validation and extraction for QBF preprocessing. Zbl 1409.68258
Heule, Marijn J. H.; Seidl, Martina; Biere, Armin
1
2017
Evaluating CDCL variable scoring schemes. Zbl 06512588
Biere, Armin; Fröhlich, Andreas
1
2015
On the complexity of symbolic verification and decision problems in bit-vector logic. Zbl 1426.68127
Kovásznai, Gergely; Veith, Helmut; Fröhlich, Andreas; Biere, Armin
1
2014
A compact representation for syntactic dependencies in QBFs. Zbl 1247.68238
Lonsing, Florian; Biere, Armin
1
2009
Simple is better: Efficient bounded model checking for past LTL. Zbl 1111.68510
Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi
1
2005
JNuke: Efficient dynamic analysis for Java. Zbl 1103.68602
Artho, Cyrille; Schuppan, Viktor; Biere, Armin; Eugster, Pascal; Baur, Marcel; Zweimüller, Boris
1
2004
Verifying the IEEE 1394 fireWire tree identify protocol with SMV. Zbl 1029.68021
Schuppan, Viktor; Biere, Armin
1
2002
Verification of out-of-order processor designs using model Checking and a light-weight completion function. Zbl 1014.68147
Berezin, Sergey; Clarke, Edmund; Biere, Armin; Zhu, Yunshan
1
2002
Strong extension-free proof systems. Zbl 07176609
Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin
1
2020
Incremental inprocessing in SAT solving. Zbl 1441.68224
Fazekas, Katalin; Biere, Armin; Scholl, Christoph
1
2019
SAT-based model checking. Zbl 1392.68232
Biere, Armin; Kröning, Daniel
4
2018
What a difference a variable makes. Zbl 1423.68419
Heule, Marijn J. H.; Biere, Armin
3
2018
Short proofs without new variables. Zbl 06778401
Heule, Marijn J. H.; Kiesl, Benjamin; Biere, Armin
3
2017
Blocked clauses in first-order logic. Zbl 1403.68240
Kiesl, Benjamin; Suda, Martin; Seidl, Martina; Tompits, Hans; Biere, Armin
2
2017
Propagation based local search for bit-precise reasoning. Zbl 1377.68134
Niemetz, Aina; Preiner, Mathias; Biere, Armin
2
2017
Solution validation and extraction for QBF preprocessing. Zbl 1409.68258
Heule, Marijn J. H.; Seidl, Martina; Biere, Armin
1
2017
Super-blocked clauses. Zbl 06623253
Kiesl, Benjamin; Seidl, Martina; Tompits, Hans; Biere, Armin
5
2016
Complexity of fixed-size bit-vector logics. Zbl 1357.68086
Kovásznai, Gergely; Fröhlich, Andreas; Biere, Armin
4
2016
SAT race 2015. Zbl 1392.68381
Balyo, Tomáš; Biere, Armin; Iser, Markus; Sinz, Carsten
2
2016
Enhancing search-based QBF solving by dynamic blocked clause elimination. Zbl 06528797
Lonsing, Florian; Bacchus, Fahiem; Biere, Armin; Egly, Uwe; Seidl, Martina
11
2015
Clause elimination for SAT and QSAT. Zbl 1336.68231
Heule, Marijn; Järvisalo, Matti; Lonsing, Florian; Seidl, Martina; Biere, Armin
11
2015
Compositional propositional proofs. Zbl 06528799
Heule, Marijn J. H.; Biere, Armin
2
2015
Evaluating CDCL variable scoring schemes. Zbl 06512588
Biere, Armin; Fröhlich, Andreas
1
2015
A unified proof system for QBF preprocessing. Zbl 1409.68257
Heule, Marijn J. H.; Seidl, Martina; Biere, Armin
12
2014
Everything you always wanted to know about blocked sets (but were afraid to ask). Zbl 1423.68435
Balyo, Tomáš; Fröhlich, Andreas; Heule, Marijn J. H.; Biere, Armin
3
2014
Detecting cardinality constraints in CNF. Zbl 1423.68437
Biere, Armin; Le Berre, Daniel; Lonca, Emmanuel; Manthey, Norbert
2
2014
On the complexity of symbolic verification and decision problems in bit-vector logic. Zbl 1426.68127
Kovásznai, Gergely; Veith, Helmut; Fröhlich, Andreas; Biere, Armin
1
2014
Factoring out assumptions to speed up MUS extraction. Zbl 1390.68601
Lagniez, Jean-Marie; Biere, Armin
6
2013
Blocked clause decomposition. Zbl 1407.68451
Heule, Marijn J. H.; Biere, Armin
5
2013
More on the complexity of quantifier-free fixed-size bit-vector logics with binary encoding. Zbl 1345.68172
Fröhlich, Andreas; Kovásznai, Gergely; Biere, Armin
5
2013
Inprocessing rules. Zbl 1358.68256
Järvisalo, Matti; Heule, Marijn J. H.; Biere, Armin
26
2012
Simulating circuit-level simplifications on CNF. Zbl 1267.94144
Järvisalo, Matti; Biere, Armin; Heule, Marijn J. H.
12
2012
Blocked clause elimination for QBF. Zbl 1341.68181
Biere, Armin; Lonsing, Florian; Seidl, Martina
18
2011
Efficient CNF simplification based on binary implication graphs. Zbl 1330.68269
Heule, Marijn J. H.; Järvisalo, Matti; Biere, Armin
11
2011
Failed literal detection for QBF. Zbl 1330.68118
Lonsing, Florian; Biere, Armin
5
2011
Blocked clause elimination. Zbl 1284.03208
Järvisalo, Matti; Biere, Armin; Heule, Marijn
25
2010
Clause elimination procedures for CNF formulas. Zbl 1306.68144
Heule, Marijn; Järvisalo, Matti; Biere, Armin
14
2010
Automated testing and debugging of SAT and QBF solvers. Zbl 1306.68155
Brummayer, Robert; Lonsing, Florian; Biere, Armin
11
2010
Integrating dependency schemes in search-based QBF solvers. Zbl 1306.68165
Lonsing, Florian; Biere, Armin
10
2010
Reconstructing solutions after blocked clause elimination. Zbl 1306.68159
Järvisalo, Matti; Biere, Armin
3
2010
Handbook of satisfiability. Zbl 1183.68568
Biere, Armin (ed.); Heule, Marijn (ed.); van Maaren, Hans (ed.); Walsh, Toby (ed.)
133
2009
Lemmas on demand for the extensional theory of arrays. Zbl 1187.68168
Brummayer, Robert; Biere, Armin
7
2009
Efficiently representing existential dependency sets for expansion-based QBF solvers. Zbl 1291.68358
Lonsing, Florian; Biere, Armin
3
2009
A compact representation for syntactic dependencies in QBFs. Zbl 1247.68238
Lonsing, Florian; Biere, Armin
1
2009
PicoSAT essentials. Zbl 1159.68403
Biere, Armin
40
2008
Nenofex: Expanding NNF for QBF solving. Zbl 1138.68546
Lonsing, Florian; Biere, Armin
10
2008
Adaptive restart strategies for conflict driven SAT solvers. Zbl 1138.68533
Biere, Armin
8
2008
Tutorial on model checking: Modelling and verification in computer science. Zbl 1171.68546
Biere, Armin
2
2008
A first step towards a unified proof checker for QBF. Zbl 1214.68334
Jussila, Toni; Biere, Armin; Sinz, Carsten; Kröning, Daniel; Wintersteiger, Christoph M.
8
2007
Compressing BMC encodings with QBF. Zbl 1277.68136
Jussila, Toni; Biere, Armin
7
2007
Linear encodings of bounded LTL model checking. Zbl 1127.68057
Biere, Armin; Heljanko, Keijo; Junttila, Tommi; Latvala, Timo; Schuppan, Viktor
14
2006
Extended resolution proofs for conjoining BDDs. Zbl 1185.68635
Sinz, Carsten; Biere, Armin
9
2006
Liveness checking as safety checking for infinite state spaces. Zbl 1273.68240
Schuppan, Viktor; Biere, Armin
7
2006
Extended resolution proofs for symbolic SAT solving with quantification. Zbl 1187.68550
Jussila, Toni; Sinz, Carsten; Biere, Armin
6
2006
Theory and applications of satisfiability testing – SAT 2006. 9th international conference, Seattle, WA, USA, August 12–15, 2006. Proceedings. Zbl 1114.68003
Biere, Armin (ed.); Gomes, Carla P. (ed.)
2
2006
Decomposing SAT problems into connected components. Zbl 1116.68079
Biere, Armin; Sinz, Carsten
2
2006
Effective preprocessing in SAT through variable and clause elimination. Zbl 1128.68463
Eén, Niklas; Biere, Armin
72
2005
Resolve and expand. Zbl 1122.68585
Biere, Armin
29
2005
Shortest counterexamples for symbolic model checking of LTL with past. Zbl 1087.68060
Schuppan, Viktor; Biere, Armin
4
2005
Simple is better: Efficient bounded model checking for past LTL. Zbl 1111.68510
Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi
1
2005
Simple bounded LTL model checking. Zbl 1117.68432
Latvala, Timo; Biere, Armin; Heljanko, Keijo; Junttila, Tommi
4
2004
JNuke: Efficient dynamic analysis for Java. Zbl 1103.68602
Artho, Cyrille; Schuppan, Viktor; Biere, Armin; Eugster, Pascal; Baur, Marcel; Zweimüller, Boris
1
2004
A satisfiability procedure for quantified Boolean formulae. Zbl 1029.68082
Plaisted, David A.; Biere, Armin; Zhu, Yunshan
4
2003
Verifying the IEEE 1394 fireWire tree identify protocol with SMV. Zbl 1029.68021
Schuppan, Viktor; Biere, Armin
1
2002
Verification of out-of-order processor designs using model Checking and a light-weight completion function. Zbl 1014.68147
Berezin, Sergey; Clarke, Edmund; Biere, Armin; Zhu, Yunshan
1
2002
Bounded model checking using satisfiability solving. Zbl 0985.68038
Clarke, Edmund; Biere, Armin; Raimi, Richard; Zhu, Yunshan
46
2001
Combining decision diagrams and SAT procedures for efficient symbolic model checking. Zbl 0974.68526
Williams, Poul F.; Biere, Armin; Clarke, Edmund M.; Gupta, Anubhav
5
2000
Verifying safety properties of a PowerPC\(^{TM}\) microprocessor using symbolic model checking without BDDs. Zbl 1046.68578
Biere, Armin; Clarke, Edmund; Raimi, Richard; Zhu, Yunshan
28
1999
all top 5

Cited by 736 Authors

21 Biere, Armin
20 Marques-Silva, João P.
12 Heule, Marijn J. H.
11 Seidl, Martina
10 Szeider, Stefan
9 Hoos, Holger H.
9 Janota, Mikoláš
9 Lonsing, Florian
8 Järvisalo, Matti
8 Schaub, Torsten H.
7 Lindauer, Marius
6 Ábrahám, Erika
6 Becker, Bernd
6 Kröning, Daniel
6 Leyton-Brown, Kevin
6 Semenov, Aleksandr Anatol’evich
5 Ansótegui, Carlos
5 Hutter, Frank
5 Kaufmann, Benjamin
5 Kiesl, Benjamin
5 Kullmann, Oliver
5 Mencía, Carlos
5 Sinz, Carsten
5 Weidenbach, Christoph
4 Balabanov, Valeriy
4 Beyersdorff, Olaf
4 Egly, Uwe
4 Gebser, Martin
4 Ignatyev, Alexey A.
4 Jiang, Jie-Hong Roland
4 Lagniez, Jean-Marie
4 Lynce, Inês
4 Philipp, Tobias
4 Saïs, Lakhdar
4 Schuppan, Viktor
4 Sebastiani, Roberto
4 Slivovsky, Friedrich
4 Stump, Aaron
4 Suda, Martin
4 Vardi, Moshe Y.
3 Amjad, Hasan
3 Balyo, Tomáš
3 Barrett, Clark W.
3 Bubeck, Uwe
3 Chew, Leroy
3 Davenport, James Harold
3 de Moura, Leonardo
3 Dodaro, Carmine
3 England, Matthew
3 Finkbeiner, Bernd
3 Ganesh, Vijay
3 Gaspers, Serge
3 Hamadi, Youssef
3 Jabbour, Said
3 Junttila, Tommi A.
3 Kauers, Manuel
3 Kleine Büning, Hans
3 Kupferman, Orna
3 Levy, Jordi
3 Manquinho, Vasco M.
3 Manthey, Norbert
3 Marić, Filip
3 Martins, Ruben
3 Niemelä, Ilkka N. F.
3 Pulina, Luca
3 Ricca, Francesco
3 Scholl, Christoph
3 Tinelli, Cesare
3 Van Gelder, Allen
3 Waldmann, Johannes
3 Wimmer, Ralf D.
3 Wintersteiger, Christoph M.
3 Zhao, Xishun
2 Alves Rocha, Thiago
2 Alviano, Mario
2 Amendola, Giovanni
2 Arif, M. Fareed
2 Asín Achá, Roberto
2 Asín, Roberto
2 Audemard, Gilles
2 Balint, Adrian
2 Banbara, Mutsunori
2 Bayless, Sam
2 Belov, Anton
2 Berg, Jeremias
2 Bersani, Marcello M.
2 Blanchette, Jasmin Christian
2 Blinkhorn, Joshua
2 Brain, Martin
2 Bright, Curtis
2 Castaño, José M.
2 Castaño, Rodrigo
2 Cimatti, Alessandro
2 Clarke, Edmund Melson jun.
2 Cook, Byron
2 Czarnecki, Krzysztof
2 Dimitrova, Rayna
2 Edelkamp, Stefan
2 Fichte, Johannes Klaus
2 Fleury, Mathias
...and 636 more Authors
all top 5

Cited in 71 Serials

35 Artificial Intelligence
29 Journal of Automated Reasoning
20 Formal Methods in System Design
17 Theoretical Computer Science
16 Constraints
8 Annals of Mathematics and Artificial Intelligence
7 Discrete Applied Mathematics
7 Theory and Practice of Logic Programming
6 Journal of Symbolic Computation
6 International Journal of Approximate Reasoning
5 Annals of Operations Research
4 Acta Informatica
4 Information Processing Letters
4 Journal of Computer and System Sciences
4 Science of Computer Programming
4 Journal of Applied Mathematics
4 Logical Methods in Computer Science
3 Automation and Remote Control
3 ACM Transactions on Computational Logic
3 Journal of Applied Logic
2 Formal Aspects of Computing
2 Machine Learning
2 Journal of Heuristics
2 Mathematical Problems in Engineering
2 Theory of Computing Systems
2 ACM Journal of Experimental Algorithmics
2 Mathematics in Computer Science
1 Computing
1 Fuzzy Sets and Systems
1 Information Sciences
1 SIAM Journal on Computing
1 Studia Logica
1 Synthese
1 Annals of Pure and Applied Logic
1 Journal of Computer Science and Technology
1 Algorithmica
1 International Journal of Parallel Programming
1 Information and Computation
1 Computers & Operations Research
1 Real-Time Systems
1 Japan Journal of Industrial and Applied Mathematics
1 Computational Geometry
1 International Journal of Algebra and Computation
1 Discrete Event Dynamic Systems
1 European Journal of Operational Research
1 Distributed Computing
1 Computational Complexity
1 Journal of Mathematical Sciences (New York)
1 Advances in Applied Clifford Algebras
1 Top
1 Nonlinear Dynamics
1 Journal of Applied Mathematics and Decision Sciences
1 Journal of Graph Algorithms and Applications
1 International Journal of Applied Mathematics and Computer Science
1 Fundamenta Informaticae
1 Computer Languages, Systems & Structures
1 4OR
1 Journal of Discrete Algorithms
1 Fuzzy Optimization and Decision Making
1 Electronic Notes in Theoretical Computer Science
1 Algorithms
1 Mathematical Programming Computation
1 Science China. Information Sciences
1 Symmetry
1 Diskretnyĭ Analiz i Issledovanie Operatsiĭ
1 Journal of Theoretical Biology
1 Frontiers of Computer Science
1 Computer Science Review
1 ACM Transactions on Computation Theory
1 Journal of Logical and Algebraic Methods in Programming
1 DML. Discrete Mathematics Letters

Citations by Year