Bloqqer swMATH ID: 9578 Software Authors: Armin Biere, Florian Lonsing, Martina Seidl Description: Blocked clause elimination for QBF. Quantified Boolean formulas (QBF) provide a powerful framework for encoding problems from various application domains, not least because efficient QBF solvers are available. Despite sophisticated evaluation techniques, the performance of such a solver usually depends on the way a problem is represented. However, the translation to processable QBF encodings is in general not unique and may either introduce variables and clauses not relevant for the solving process or blur information which could be beneficial for the solving process. To deal with both of these issues, preprocessors have been introduced which rewrite a given QBF before it is passed to a solver. In this paper, we present novel preprocessing methods for QBF based on blocked clause elimination (BCE), a technique successfully applied in SAT. Quantified blocked clause elimination (QBCE) allows to simulate various structural preprocessing techniques as BCE in SAT. We have implemented QBCE and extensions of QBCE in the preprocessor bloqqer. In our experiments we show that preprocessing with QBCE reduces formulas substantially and allows us to solve considerable more instances than the previous state-of-the-art Homepage: http://fmv.jku.at/bloqqer/ Related Software: DepQBF; MiniSat; sQueezeBF; Quaffle; semprop; CAQE; Nenofex; QUBOS; Quantor; Lingeling; sKizzo; PicoSAT; QUBE; QBFLIB; QRATPre+; HQSpre; DRAT-trim; ABC; Treengeling; Plingeling Cited in: 31 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Blocked clause elimination for QBF. Zbl 1341.68181Biere, Armin; Lonsing, Florian; Seidl, Martina 2011 all top 5 Cited by 57 Authors 10 Seidl, Martina 9 Lonsing, Florian 7 Biere, Armin 5 Egly, Uwe 4 Janota, Mikoláš 4 Marques-Silva, João P. 3 Heule, Marijn J. H. 3 Kiesl, Benjamin 3 Slivovsky, Friedrich 3 Szeider, Stefan 2 Bacchus, Fahiem 2 Clarke, Edmund Melson jun. 2 Jiang, Jie-Hong Roland 2 Klieber, William 2 Peitl, Tomáš 2 Rabe, Markus N. 2 Scholl, Christoph 2 Tompits, Hans 2 Van Gelder, Allen 1 Balabanov, Valeriy 1 Balyo, Tomáš 1 Becker, Bernd 1 Belov, Anton 1 Beyersdorff, Olaf 1 Bloem, Roderick 1 Braud-Santoni, Nicolas 1 Brayton, Robert K. 1 Chew, Leroy 1 Fandinno, Jorge 1 Faymonville, Peter 1 Finkbeiner, Bernd 1 Gitina, Karina 1 Goultiaeva, Alexandra 1 Grigore, Radu 1 Hadzic, Vedad 1 Hsu, Tzu-Chien 1 Kronegger, Martin 1 Laferriere, Francois 1 Linsbichler, Thomas 1 Lynce, Inês 1 Maratea, Marco 1 Mishchenko, Alan 1 Niskanen, Andreas 1 Nist, Jennifer 1 Pfandler, Andreas 1 Pulina, Luca 1 Romero, Javier 1 Schaub, Torsten H. 1 Seshia, Sanjit Arunkumar 1 Son, Tran Cao 1 Sreenivasaiah, Karteek 1 Tentrup, Leander 1 Tu, Kuan-Hua 1 Wallner, Johannes Peter 1 Wimmer, Ralf D. 1 Woltran, Stefan 1 Wood, Samuel B. all top 5 Cited in 7 Serials 5 Artificial Intelligence 3 Journal of Automated Reasoning 1 Journal of Computer and System Sciences 1 Formal Methods in System Design 1 Annals of Mathematics and Artificial Intelligence 1 Theory and Practice of Logic Programming 1 Logical Methods in Computer Science Cited in 2 Fields 31 Computer science (68-XX) 11 Mathematical logic and foundations (03-XX) Citations by Year