HQS
| Beteiligte Mitarbeiter | Kooperationspartner | Projektbeschreibung | Software | Benchmarks | Publikationen
|
| Lehrstuhl für Betriebssysteme | |
| Aile Ge-Ernst, M.Sc. | |
| Christoph Scholl, Prof. Dr. | |
|
| |
| Concept Engineering | |
| Ralf Wimmer | |
Unser Solver HQS ist ein DQBF-Solver, welcher auf Quantorenelimination basiert. Die grundlegende Idee ist es, eine Menge von Abhängigkeiten zu finden, die eliminiert oder hinzuzufügt werden soll, um eine kleinstmögliche erfüllbarkeitsäquivalente QBF aus einer DQBF zu gewinnen. Die so entstandene QBF wird anschließend weiter verarbeitet.
Der integrierte Präprozessor HQSpre ist das erste State-of-the-Art-Tool um DQBFs zu vereinfachen. Es verwendet die meisten Vorverarbeitungstechniken, die in der Literatur vorgestellt werden, so wie z. B. BCP, Equivalence Checking, Gattererkennung. Es kann sowohl als Stand-Alone-Tool als auch als Bibliothek verwendet werden.
HQS
HQS ist ein moderner QBF/DQBF-Solver. Es wurde im Rahmen vom DFG-Projekt "" Lösen von Abhängigkeitsquantifizierten Booleschen Formeln (DQBF)" entwickelt. Für weitere Informationen zum Projekt siehe hier.
Parametrisierte DQBF mit disjunkten Abhängigkeitsmengen
DQBF-Instanzen von QBFEval18
DQBF-Instanzen generiert aus pec, synthesis etc.
|
Karina Gitina, Sven Reimer, Matthias Sauer, Ralf Wimmer, Christoph Scholl, Bernd Becker Equivalence checking of partial designs using dependency quantified Boolean formulae Proceedings of the 31st IEEE International Conference on Computer Design, pages 396–403, IEEE Computer Society Press |
|
Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd Becker Preprocessing for DQBF 2015 Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT), Springer-Verlag, issue: 9340, pages: 173 - 190 |
|
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 |
|
Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker Dependency Schemes for DQBF 2016 Proceedings of the 19th International Conference on Theory and Applications of Satisfiability Testing (SAT) |
|
Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker From DQBF to QBF by Dependency Elimination Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT) |
|
Karina Wimmer, Ralf Wimmer, Christoph Scholl, Bernd Becker Skolem Functions for DQBF Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA) |
|
Ralf Wimmer, Sven Reimer, Paolo Marin, Bernd Becker HQSpre – An Effective Preprocessor for QBF and DQBF Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) |
|
Ralf Wimmer, Karina Wimmer, Christoph Scholl, Bernd Becker Analysis of Incomplete Circuits using Dependency Quantified Boolean Formulas Advanced Logic Synthesis |
|
Aile Ge-Ernst, Christoph Scholl, Ralf Wimmer Localizing Quantifiers for DQBF 2019 Proceedings of the Conference on Formal Methods in Computer Aided Design (FMCAD), IEEE Computer Society Press |
|
Christoph Scholl, Ralf Wimmer Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications Proceedings of 21th International Conference on Theory and Applications of Satisfiability Testing (SAT 2018) |
|
Christoph Scholl, Jie-Hong Roland Jiang, Ralf Wimmer, Aile Ge-Ernst A PSPACE Subclass of Dependency Quantified Boolean Formulas and Its Effective Solving Proceedings of 33th AAAI Conference on Artificial Intelligence (AAAI-19) |
|
Ralf Wimmer, Christoph Scholl, Bernd Becker The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation 2019 Journal on Satisfiability, Boolean Modeling and Computation, Band: 11, Nummer: 1, Seiten: 3 - 52 |