2012

 back to the year overview

• Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd Becker
  Enhanced Integration of QBF Solving Techniques
  2012 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, pages: 133 - 143
  » show abstract« hide abstract
  Abstract

  In this paper we present a novel QBF solving technique which is based on the integration of a search based (DPLL) and a rewriting based approach: While traversing the search space in a DPLL manner, we iteratively generate many sub-problems, which are handed over to the rewriting method one by one. Instead of just communicating back satisfiability results of the individual sub-problems, we collect as many constraints derived by the rewriting based solver as possible, and transfer them back to the search based solver. This allows not only to prune the current branch, but also to avoid the unnecessary traversal of search paths in different regions of the search tree. We also discuss heuristics to determine suitable switching points between these two methods. We present first promising results that underline the potential of our approach.

2011

 back to the year overview

• Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd Becker
  Integration of Orthogonal QBF Solving Techniques
  2011 Conf. on Design, Automation and Test in Europe, pages: 149 - 154
  » show abstract« hide abstract
  Abstract

  In this paper we present a method for integrating two complementary solving techniques for QBF formulas, i. e. variable elimination based on an AIG-framework and search with DPLL based solving. We develop a sophisticated mechanism for coupling these techniques, enabling the transfer of partial results from the variable elimination part to the search part. This includes the definition of heuristics to (1) determine appropriate points in time to snapshot the current partial result during variable elimination (by estimating its quality) and (2) switch from variable elimination to search-based methods (applied to the best known snapshot) when the progress of variable elimination is supposed to be too slow or when representation sizes grow too fast. We will show in the experimental section that our combined approach is clearly superior to both individual methods run in a stand-alone manner. Moreover, our combined approach significantly outperforms all other state-of-the-art solvers.

2009

 back to the year overview

• Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid
  Computing Optimized Representations for Non-convex Polyhedra by Detection and Removal of Redundant Linear Constraints
  2009 Tools and Algorithms for the Construction and Analysis of Systems, Springer, volume: 5505, pages: 383 - 397
  » show abstract« hide abstract
  Abstract

  We present a method which computes optimized representationsfor non-convex polyhedra. Our method detects so-called redundantlinear constraints in these representations by using an incremental SMT(Satisfiability Modulo Theories) solver and then removes the redundantconstraints based on Craig interpolation. The approach is motivated byapplications in the context of model checking for Linear Hybrid Automata.Basically, it can be seen as an optimization method for formulasincluding arbitrary boolean combinations of linear constraints andboolean variables. We show that our method provides an essential stepmaking quantifier elimination for linear arithmetic much more efficient.Experimental results clearly show the advantages of our approach incomparison to state-of-the-art solvers.

2008

 back to the year overview

• Christoph Scholl, Stefan Disch, Florian Pigorsch, Stefan Kupferschmid
  Using an SMT Solver and Craig Interpolation to Detect and Remove Redundant Linear Constraints in Representations of Non-Convex Polyhedra
  2008 Int'l Workshop on Satisfiability Modulo Theories, pages: 18 - 26