Sven Reimer, Dr.
Technische Fakultät Albert-Ludwigs-Universität Georges Köhler Allee, Gebäude 051 79110 Freiburg im Breisgau Deutschland
Gebäude 51, Raum 01..030
++49 +761 203-8156
reimer@informatik.uni-freiburg.de
Sven Reimer
Liste filtern : Jahre: 2018 |
2017 |
2016 |
2015 |
2014 |
2013 |
2012 |
2011 | alle anzeigen nach oben zur Jahresübersicht Tobias Paxian, Sven Reimer, Bernd BeckerDynamic Polynomial Watchdog Encoding for Solving Weighted MaxSAT 2018 International Conference on Theory and Applications of Satisfiability Testing , Springer, Band : 10929, Seiten : 37 - 53» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung In this paper we present a novel pseudo-Boolean (PB) constraint encoding for solving the weighted MaxSAT problem with iterative SAT-based methods based on the Polynomial Watchdog (PW) CNF encoding. The watchdog of the PW encoding indicates whether the bound of the PB constraint holds. In our approach, we lift this static watchdog concept to a dynamic one allowing an incremental convergence to the optimal result. Consequently, we formulate and implement a SAT-based algorithm for our new Dynamic Polynomial Watchdog (DPW) encoding which can be applied for solving the MaxSAT problem. Furthermore, we introduce three fundamental optimizations of the PW encoding also suited for the original version leading to significantly less encoding size.
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. nach oben zur Jahresübersicht Ralf Wimmer, Sven Reimer, Paolo Marin, Bernd BeckerHQSpre - 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, Band : 10205, Seiten : 373 - 390» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 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. nach oben zur Jahresübersicht Matthias Sauer, Jie Jiang, Sven Reimer, Kohei Miyase, Xiaoqing Wen, Bernd Becker, Ilia PolianOn 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 BeckerClock Cycle Aware Encoding for SAT-based Circuit Initialization 2016 GI/ITG Workshop “Testmethoden und Zuverlässigkeit von Schaltungen und Systemen” nach oben zur Jahresübersicht Dominik Erb, Michael A. Kochte, Sven Reimer, Matthias Sauer, Hans-Joachim Wunderlich, Bernd BeckerAccurate QBF-based Test Pattern Generation in Presence of Unknown Values 2015 Computer-Aided Design of Integrated Circuits and Systems (TCAD) » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung Unknown (X) values emerge during the design process as well as during system operation and test application. X-sources are for instance black boxes in design models, clockdomain boundaries, analog-to-digital converters, or uncontrolled or uninitialized sequential elements.
To compute a test pattern for a given fault, well-defined logic values are required both for fault activation and Propagation to observing outputs. In presence of X-values, conventional test generation algorithms, based on structural algorithms, Boolean satisfiability (SAT), or BDD-based reasoning may fail to generate test patterns or to prove faults untestable.
This work proposes the first efficient stuck-at and transition-delay fault test generation algorithm able to prove testability or untestability of faults in presence of X-values. It overcomes the principal pessimism of conventional algorithms when X-values are considered by mapping the test generation problem to the satisfiability of Quantified Boolean Formulae (QBF).
Experiments on ISCAS benchmarks and larger industrial
circuits investigate the increase in fault coverage for conventional deterministic and potential detection requirements for both randomized and clustered X-sources. Der Andere Verlag , Seite : 174Bekannte 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 BeckerSolving DQBF Through Quantifier Elimination 2015 Conf. on Design, Automation and Test in Europe nach oben zur Jahresübersicht Sven Reimer, Matthias Sauer, Tobias Schubert, Bernd BeckerIncremental Encoding and Solving of Cardinality Constraints 2014 International Symposium on Automated Technology for Verification and Analysis , Springer International Publishing, Band : 8837, Seiten : 297 - 313» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 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 BeckerQBF with Soft Variables 2014 International Workshop on Automated Verification of Critical Systems (AVOCS) Matthias Sauer, Sven Reimer, Sudhakar M. Reddy, Bernd BeckerEfficient SAT-based Circuit Initialization for Large Designs 2014 Int'l Conf. on VLSI Design » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 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 BeckerUsing MaxBMC for Pareto-Optimal Circuit Initialization
2014 Conf. on Design, Automation and Test in Europe » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 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. nach oben zur Jahresübersicht Matthias Sauer, Sven Reimer, Stefan Kupferschmid, Tobias Schubert, Paolo Marin, Bernd BeckerApplying 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 » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We present an approach to identify functional input sequences
in sequential circuits. The properties required are inserted as target of
a bounded model checking (BMC) problem, by using Craig interpolants
it can be stated whether sequences justifying the properties exist or
not. The initial state is either completely or partially unknown, and for
the latter we engage a MAX-SAT formulation to retrieve the shortest
sequence if a maximal subset of the initial state bits are unknown.
We apply this method to problems arising from digital circuit testing
domain, in which usually an arbitrary initial state is assumed, i.e., that
the circuit’s sequential elements (ﬂip-ﬂops) are assumed to be fully con-
trollable. However, since some of these states may be unreachable during
normal operation, this results in undesired secondary test conditions.
In this paper BMC is used to (1) test timing faults in a digital circuit,
thereby the test requirements are encoded as target properties. Our
method yields the shortest functional test-sequences that justify the target
properties or it proves that such a sequence does not exist. Furthermore,
(2) the initialization of circuits is considered. We analyze the length of
such sequences depending on the number of controllable ﬂip-ﬂops. Matthias Sauer, Sven Reimer, Tobias Schubert, Ilia Polian, Bernd BeckerEfficient SAT-Based Dynamic Compaction and Relaxation for Longest Sensitizable Paths 2013 Conf. on Design, Automation and Test in Europe , Seiten : 448 - 453» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 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 BeckerEquivalence 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, Seiten : 61 - 70» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 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 BeckerEquivalence Checking of Partial Designs using Dependency Quantified Boolean Formulae 2013 Int'l Conf. on Computer Design , IEEE Computer Society, Seiten : 396 - 403» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung We consider the partial equivalence checking problem (PEC), i.e., checking whether a given partial implementation of a combinational circuit can (still) be extended to a complete design that is equivalent to a given full specification. To solve PEC, we give a linear transformation from PEC to the question whether a dependency quantified Boolean formula (DQBF) is satisfied.
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 BeckerProvably Optimal Test Cube Generation Using Quantified Boolean Formula Solving 2013 ASP Design Automation Conf. » Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 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. nach oben zur Jahresübersicht Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd BeckerEnhanced Integration of QBF Solving Techniques 2012 GI/ITG/GMM Workshop “Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen” , Seiten : 133 - 143» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 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. nach oben zur Jahresübersicht Sven Reimer, Florian Pigorsch, Christoph Scholl, Bernd BeckerIntegration of Orthogonal QBF Solving Techniques 2011 Conf. on Design, Automation and Test in Europe , Seiten : 149 - 154» Kurzfassung anzeigen « Kurzfassung verbergen Kurzfassung 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.