2017

 back to the year overview

• Ralf Wimmer, Sven Reimer, Paolo Marin, Bernd Becker
  HQSpre - An Effective Preprocessor for QBF and DQBF
  2017 Uppsala, Sweden International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Part I, Axel Legay and Tiziana Margaria, volume: 10205, pages: 373 - 390
  » show abstract« hide abstract
  Abstract

  We present our new preprocessor \textsc{HQSpre}, a state-of-the-art tool for simplifying quantified Boolean formulas (QBFs) and the first available preprocessor for dependency quantified Boolean formulas (DQBFs). The latter are a generalization of QBFs, resulting from adding so-called Henkin-quantifiers to QBFs. HQSpre applies most of the preprocessing techniques that have been proposed in the literature. It can be used both as a standalone tool and as a library. It is possible to tailor it towards different solver back-ends, e. g., to preserve the circuit structure of the formula when a non-CNF solver back-end is used. Extensive experiments show that HQSpre allows QBF solvers to solve more benchmark instances and is able to decide more instances on its own than state-of-the-art tools. The same impact can be observed in the DQBF domain as well.

2016

 back to the year overview

• Paolo Marin, Massimno Narizzano, Luca Pulina, Armando Tacchella, Enrico Giunchiglia
  Twelve Years of QBF Evaluations: QSAT Is PSpace-Hard and It Shows
  2016 Fund Inform, volume: 149, issue: 1-2, pages: 133 - 158

2015

 back to the year overview

• Paolo Marin, Massimo Narizzano, Luca Pulina, Armando Tacchella, Enrico Giunchiglia
  An Empirical Perspective on Ten Years of QBF Solving
  2015 22nd RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion 2015 (RCRA 2015) Proceedings of the 22nd RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion (RCRA 2015), CEUR-WS.org, volume: 1451, pages: 62 - 75
• Christian Miller, Paolo Marin, Bernd Becker
  Verification of Partial Designs Using Incremental QBF
  2015 Ai Commun, volume: 28, issue: 2, pages: 283 - 307
  » show abstract« hide abstract
  Abstract

  SAT solving is an indispensable core component of numerous formal verification tools and has found widespread use in industry, in particular when using it in an incremental fashion, e.g. in Bounded Model Checking (BMC). On the other hand, for some applications SAT formulas are not expressive enough, whereas a description via Quantified Boolean Formulas (QBF) is much more adequate, for instance when dealing with partial designs. Motivated by the success of incremental SAT, in this paper we explore various approaches to solve QBF problems in an incremental fashion and thereby make this technology usable as a core component of BMC. Firstly, we realized an incremental QBF solver based on the state-of-the-art QBF solver QuBE: Taking profit from the reuse of some information from previous iterations, the search space can be pruned, in some cases, to even less than a quarter. However, the need for preprocessing QBF formulas prior to the solving phase, that in general cannot be paired with incremental solving because of the non-predictable elimination of variables in the future incremental steps, posed the question of incremental QBF preprocessing. In this context we present an approach for retaining the QBF formula being preprocessed while extending its clauses and prefix incrementally. This procedure results in a significant size reduction of the QBF formulas, hence leading to a reduced solving time. As this may come together with a high preprocessing time, we analyze various heuristics to dynamically disable incremental preprocessing when its overhead raises over a certain threshold and is not compensated by the reduced solving time anymore. For proving the efficacy of our methods experimentally, as an application we consider BMC for partial designs (i.e. designs containing so-called blackboxes which represent unknown parts). Here, we disprove realizability, that is, we prove that an unsafe state is reachable no matter how the blackboxes are implemented. We examine all these incremental approaches from both the point of view of the effectiveness of the single procedure and the benefits that a range of QBF solvers can take from it. On a domain of partial design benchmarks, engaging incremental QBF methods significant performance gains over non incremental BMC can be achieved.

2014

 back to the year overview

• Sven Reimer, Matthias Sauer, Paolo Marin, Bernd Becker
  QBF with Soft Variables
  2014 International Workshop on Automated Verification of Critical Systems (AVOCS)

2013

 back to the year overview

• Matthias Sauer, Sven Reimer, Stefan Kupferschmid, Tobias Schubert, Paolo Marin, Bernd Becker
  Applying BMC, Craig Interpolation and MAX-SAT to Functional Justification in Sequential Circuits
  2013 RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
  » show abstract« hide abstract
  Abstract

  such sequences depending on the number of controllable flip-flops.

2012

 back to the year overview

• Christian Miller, Paolo Marin, Bernd Becker
  A Dynamic QBF Preprocessing Approach for the Verification of Incomplete Designs
  2012 Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion, volume: 19
  » show abstract« hide abstract
  Abstract

  preprocessing effectiveness does not compensate for the time spent. We present multiple switching heuristics, and evaluate the overall performance by running several state-of-the-art QBF solvers as back-end. Comparing these results to those obtained by standard and incremental BMC procedures it turns out that dynamic preprocessing leads to the best overall performance of the whole verification process.
• Bernd Becker, Ruediger Ehlers, Matthew Lewis, Paolo Marin
  ALLQBF Solving by Computational Learning
  2012 Automated Technology for Verification and Analysis, Springer, volume: 7561, pages: 370 - 384
  » show abstract« hide abstract
  Abstract

  In the last years, search-based QBF solvers have become essential formany applications in the formal methods domain. The exploitation oftheir reasoning efficiency has however been restricted to applicationsin which a ``satisfiable/unsatisfiable'' answer or one model of anopen quantified Boolean formula suffices as an outcome, whereasapplications in which a compact representation of all models isrequired could not be tackled with QBF solvers so far. In this paper,we describe how computational learning provides a remedy to thisproblem. Our algorithms employ a search-based QBF solver and learn theset of all models of a given open QBF problem in a CNF (conjunctivenormal form), DNF (disjunctive normal form), or CDNF (conjunction ofDNFs) representation. We evaluate our approach experimentally usingbenchmarks from synthesis of finite-state systems from temporal logicand monitor computation.
• Paolo Marin, Christian Miller, Bernd Becker
  Incremental QBF Preprocessing for Partial Design Verification - (Poster Presentation)
  2012 Int'l Conf. on Theory and Applications of Satisfiability Testing, Springer, volume: 7317, pages: 473 - 474
  » show abstract« hide abstract
  Abstract

  Bounded Model Checking (BMC) is a major verification method for finding errors in sequential circuits. BMC accomplishes this by iteratively unfolding a circuit k times, adding the negated property, and finally converting the BMC instance into a sequence of satisfiability (SAT) problems. When considering incomplete designs (i.e. those containing so-called blackboxes), we rather need the logic of Quantified Boolean Formulas (QBF) to obtain a more precise modeling of the unknown behavior of the blackbox. Here, we answer the question of unrealizability of a property, where finding a path of length k proves that the property is violated regardless of the implementation of the blackbox. To boost this task, solving blackbox BMC problems incrementally has been shown to be feasible [3], although the restrictions required in the preprocessing phase reduce its effectiveness. In this paper we enhance the verification procedure when using an off-the-shelf QBF solver, through a stronger preprocessing of the QBF formulas applied in an incremental fashion.
• Paolo Marin, Christian Miller, Matthew Lewis, Bernd Becker
  Verification of Partial Designs Using Incremental QBF Solving
  2012 Conf. on Design, Automation and Test in Europe, pages: 623 - 628
  » show abstract« hide abstract
  Abstract

  SAT solving is an indispensable core component of numerous formal verification tools and has found widespread use in industry, in particular when using it in an incremental fashion, e.g. in Bounded Model Checking (BMC). On the other hand, there are applications, in particular in the area of partial design verification, where SAT formulas are not expressive enough and a description via Quantified Boolean Formulas (QBF) is much more adequate.In this paper we introduce incremental QBF solving and thereby make it usable as a core component of BMC. To do so, we realized an incremental version of the state-of-the-art QBF solver QuBE, allowing for the reuse of learnt information e.g. in the form of conflict clauses and solution cubes. As an application we consider BMC for partial designs (i.e. designs containing so-called blackboxes) and thereby disprove realizability, that is, we prove that an unsafe state is reachable no matter how the blackboxes are implemented. In our experimental analysis, we compare different incremental approaches implemented in our BMC tool. BMC with incremental QBF turns out to be feasible for designs with more than 21,000 gates and 2,700 latches. Significant performance gains over non incremental QBF based BMC can be obtained on many benchmark circuits, in particular when using the so-called backward-incremental approach combined with incremental preprocessing.

2011

 back to the year overview

• Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico Giunchiglia
  Parallel QBF Solving with Advanced Knowledge Sharing
  2011 Fundamenta Informaticae, volume: 107, issue: 2-3, pages: 139 - 166
  » show abstract« hide abstract
  Abstract

  In this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited from modern computer architectures, from pervasive multi-core boxes to clusters and grids, to solve more relevant instances faster than previous generation solvers. Furthermore, PaQuBE's progressive MPI based parallel framework is the first to support advanced knowledge sharing in which solution cubes as well as conflict clauses can be exchanged between solvers. Knowledge sharing plays a critical role in the performance of PaQuBE. However, due to the overhead associated with sending and receiving MPI messages, and the restricted communication/network bandwidth available between solvers, it is essential to optimize not only what information is shared, but the way in which it is shared. In this context, we compare multiple conflict clause and solution cube sharing strategies, and finally show that an adaptive method provides the best overall results.

2010

 back to the year overview

• Paolo Marin, Enrico Giunchiglia, Massimo Narizzano
  Conflict and Solution Driven Constraint Learning in QBF
  2010 Doctoral Programme CP 2010
  » show abstract« hide abstract
  Abstract

  search based QBF solver.
• Enrico Giunchiglia, Paolo Marin, Massimo Narizzano
  QuBE7.0, System Description
  2010 Journal of Satisfiability, volume: 7, issue: 8, pages: 83 - 88
  » show abstract« hide abstract
  Abstract

  In this paper we outline QuBE7’s main features, describing first the options of the preprocessors, and then giving some details about how the core search-based solver (i) performs unit and pure literal propagation; and (ii) performs the “Conflict Analysis procedure” for non-chronological backtracking, generalised from the SAT to the QBF case. We conclude with the experimental evaluation, showing that QuBE7.0 is the a state-of-the-art single-engine QBF solver.
• Enrico Giunchiglia, Paolo Marin, Massimo Narizzano
  sQueezeBF: An effective preprocessor for QBFs
  2010 Theory and Applications of Satisfiability Testing, Springer Verlag, volume: 6175, pages: 85 - 98
  » show abstract« hide abstract
  Abstract

  In this paper we present sQueezeBF, an effective preprocessor for QBFs that combines various techniques for eliminating variables and/or redundant clauses. In particular sQueezeBF combines (i) variable elimination via Q-resolution, (ii) variable elimination via equivalence substitution and (iii) equivalence breaking via equivalence rewriting. The experimental analysis shows that sQueezeBF can produce significant reductions in the number of clauses and/or variables - up to the point that some instances are solved directly by sQueezeBF - and that it can significantly improve the efficiency of a range of state-of-the-art QBF solvers - up to the point that some instances cannot be solved without sQueezeBF preprocessing.

2009

 back to the year overview

• Paolo Marin, Matthew Lewis, Massimo Narizzano, Tobias Schubert, Enrico Giunchiglia, Bernd Becker
  Comparison of Knowledge Sharing Strategies in a Parallel QBF Solver
  2009 High-Performance Computing and Simulation Conference, pages: 161 - 167
• Paolo Marin, Matthew Lewis, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico Giunchiglia
  Evaluation of Knowledge Sharing Strategies in a Parallel QBF Solver
  2009 RCRA International Workshop on Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion
• Matthew Lewis, Paolo Marin, Tobias Schubert, Massimo Narizzano, Bernd Becker, Enrico Giunchiglia
  PaQuBE: Distributed QBF Solving with Advanced Knowledge Sharing
  2009 Int'l Conf. on Theory and Applications of Satisfiability Testing, volume: 5584, pages: 509 - 523

2008

 back to the year overview

• Enrico Giunchiglia, Paolo Marin, Massimo Narizzano
  An Effective Preprocessor for QBF pre-reasoning
  2008 Int'l Workshop on Quantification in Constraint Programming