2018

 back to the year overview

• Tobias Paxian, Sven Reimer, Bernd Becker
  Dynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT
  2018 International Conference on Theory and Applications of Satisfiability Testing, Springer, volume: 10929, pages: 37 - 53
  » show abstract« hide abstract
  Abstract

  Our experimental results show that our encoding and algorithm is competitive with state-of-the-art encodings as utilized in QMaxSAT (2nd place in last MaxSAT Evaluation 2017). Our encoding dominates two of the QMaxSAT encodings, and at the same time is able to solve unique instances. We integrated our new encoding into QMaxSAT and adapt the heuristic to choose between the only remaining encoding of QMaxSAT and our approach. This combined version solves 19 (4%) more instances in overall 30\% less run time on the benchmark set of the MaxSAT Evaluation 2017. Compared to each encoding of QMaxSAT used in the evaluation, our encoding leads to an algorithm that is on average at least 2X faster.

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

• Matthias Sauer, Jie Jiang, Sven Reimer, Kohei Miyase, Xiaoqing Wen, Bernd Becker, Ilia Polian
  On Optimal Power-aware Path Sensitization
  2016 2016 25nd IEEE Asian Test Symposium (ATS)
• Matthias Sauer, Sven Reimer, Daniel Tille, Karsten Scheibler, Dominik Erb, Ulrike Pfannkuchen, Bernd Becker
  Clock Cycle Aware Encoding for SAT-based Circuit Initialization
  2016 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen”

2015

 back to the year overview

• Dominik Erb, Michael A. Kochte, Sven Reimer, Matthias Sauer, Hans-Joachim Wunderlich, Bernd Becker
  Accurate QBF-based Test Pattern Generation in Presence of Unknown Values
  2015 Computer-Aided Design of Integrated Circuits and Systems (TCAD)
  » show abstract« hide abstract
  Abstract

  circuits investigate the increase in fault coverage for conventional deterministic and potential detection requirements for both randomized and clustered X-sources.
• Der Andere Verlag, page: 174
  Bekannte Unbekannte - Formale Methoden in Anwesenheit unbekannter Werte
  ISBN: 978-3-86247-569-8
  Sven Reimer
• Karina Gitina, Ralf Wimmer, Sven Reimer, Matthias Sauer, Christoph Scholl, Bernd Becker
  Solving DQBF Through Quantifier Elimination
  2015 Conf. on Design, Automation and Test in Europe

2014

 back to the year overview

• Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd Becker
  Incremental Encoding and Solving of Cardinality Constraints
  2014 International Symposium on Automated Technology for Verification and Analysis, Springer International Publishing, volume: 8837, pages: 297 - 313
  » show abstract« hide abstract
  Abstract

  Traditional SAT-based MaxSAT solvers encode cardinality constraints directly as part of the CNF and solve the entire optimization problem by a sequence of iterative calls of the underlying SAT solver. The main drawback of such approaches is their dependence on the number of soft clauses: The more soft clauses the MaxSAT instance contains, the larger is the CNF part encoding the cardinality constraints. To counter this drawback, we introduce an innovative encoding of cardinality constraints: Instead of translating the entire and probably bloated constraint network into CNF, a divide-and-conquer approach is used to encode partial constraint networks successively. The resulting subproblems are solved and merged incrementally, reusing not only intermediate local optima, but also additional constraints which are derived from solving the individual subproblems by the back-end SAT solver. Extensive experimental results for the last MaxSAT evaluation benchmark suitew demonstrate that our encoding is in general smaller compared to existing methods using a monolithic encoding of the constraints and converges faster to the global optimum.
• Sven Reimer, Matthias Sauer, Paolo Marin, Bernd Becker
  QBF with Soft Variables
  2014 International Workshop on Automated Verification of Critical Systems (AVOCS)
• Matthias Sauer, Sven Reimer, Sudhakar M. Reddy, Bernd Becker
  Efficient SAT-based Circuit Initialization for Large Designs
  2014 Int'l Conf. on VLSI Design
  » show abstract« hide abstract
  Abstract

  We present a procedure to determine initialization sequences for a sequential circuit optimizing sequence length and unknown values (Xes) in the flip-flops. Specifically, we consider the following two problems: (1) Determine a sequence that initializes a maximal set of flip-flops starting in a completely unknown state. (2) Determine a minimal subset of flip-flops that need to be controllable such that the circuit can be completely initialized in a limited number of time frames. The underlying principle of our methods is a maximization formalism using formal optimization techniques based on satisfiability solvers (MaxSAT). We introduce several heuristics which increase the scalability of our approach significantly. Experimental results demonstrate the applicability of the method for large academic and industrial benchmark circuits with up to a few hundred thousand gates.
• Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd Becker
  Using MaxBMC for Pareto-Optimal Circuit Initialization
  2014 Conf. on Design, Automation and Test in Europe
  » show abstract« hide abstract
  Abstract

  In this paper we present MaxBMC, a novel formalism for solving optimization problems in sequential systems. Our approach combines techniques from symbolic SAT-based Bounded Model Checking (BMC) and incremental MaxSAT, leading to the first MaxBMC solver. In traditional BMC safety and liveness properties are validated. We extend this formalism: in case the required property is satisfied, an optimization problem is defined to maximize the quality of the reached witnesses. Further, we compare its qualities in different depths of the system, leading to Pareto-optimal solutions. We state a sound and complete algorithm that not only tackles the optimization problem but moreover verifies whether a global optimum has been identified by using a complete BMC solver as back-end. As a first reference application we present the problem of circuit initialization. Additionally, we give pointers to other tasks which can be covered by our formalism quite naturally and further demonstrate the efficiency and effectiveness of our approach.

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.
• Matthias Sauer, Sven Reimer, Tobias Schubert, Ilia Polian, Bernd Becker
  Efficient SAT-Based Dynamic Compaction and Relaxation for Longest Sensitizable Paths
  2013 Conf. on Design, Automation and Test in Europe, pages: 448 - 453
  » show abstract« hide abstract
  Abstract

  Comprehensive coverage of small-delay faults under massive process variations is achieved when multiple paths through the fault locations are sensitized by the test pair set. Using one test pair per path may lead to impractical test set sizes and test application times due to the large number of near-critical paths in state-of-the-art circuits.
• Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker
  Equivalence Checking for Partial Implementations Revisited
  2013 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen”, Universität Rostock ITMZ, pages: 61 - 70
  » show abstract« hide abstract
  Abstract

  In this paper we consider the problem of checking whether a partial implementation can (still) be extended to a complete design which is equivalent to a given full specification. In particular, we investigate the relationship between the equivalence checking problem for partial implementations (PEC) and the validity problem for quantified boolean formulae (QBF) with so-called Henkin quantifiers. Our analysis leads us to a sound and complete algorithmic solution to the PEC problem as well as to an exact complexity theoretical classification of the problem.
• Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker
  Equivalence Checking of Partial Designs using Dependency Quantified Boolean Formulae
  2013 Int'l Conf. on Computer Design, IEEE Computer Society, pages: 396 - 403
  » show abstract« hide abstract
  Abstract

  Our novel algorithm to solve DQBF based on quantifier elimination can therefore be applied to solve PEC. We also present first experimental results showing the feasibility of our approach and the inaccuracy of QBF approximations, which are usually used for deciding the PEC so far.
• Matthias Sauer, Sven Reimer, Ilia Polian, Tobias Schubert, Bernd Becker
  Provably Optimal Test Cube Generation Using Quantified Boolean Formula Solving
  2013 ASP Design Automation Conf.
  » show abstract« hide abstract
  Abstract

  Circuits that employ test pattern compression rely on test cubes to achieve high compression ratios. The less inputs of a test pattern are specified, the better it can be compacted and hence the lower the test application time. Although there exist previous approaches to generate such test cubes, none of them are optimal. We present for the first time a framework that yields provably optimal test cubes by using the theory of quantified Boolean formulas (QBF). Extensive comparisons with previous methods demonstrate the quality gain of the proposed method.

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.