SAT-Based Synthesis Methods for Safety Specs
From MaRDI portal
Publication:2938057
DOI10.1007/978-3-642-54013-4_1zbMath1428.68040arXiv1311.3530OpenAlexW1922664086MaRDI QIDQ2938057
Martina Seidl, Roderick Bloem, Robert Könighofer
Publication date: 13 January 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1311.3530
Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Mathematical problems of computer architecture (68M07)
Related Items
Solution validation and extraction for QBF preprocessing, The QBF Gallery: behind the scenes, Labelled interpolation systems for hyper-resolution, clausal, and local proofs, Solving dependency quantified Boolean formulas using quantifier localization, Long-distance Q-resolution with dependency schemes, Unnamed Item, Synchronous counting and computational algorithm design, Tableaux for realizability of safety specifications, Unnamed Item, Indecision and delays are the parents of failure -- taming them algorithmically by synthesizing delay-resilient control, Encodings of Bounded Synthesis, A symbolic algorithm for lazy synthesis of eager strategies, Dependency Schemes for DQBF, Long Distance Q-Resolution with Dependency Schemes, Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations, Reinterpreting dependency schemes: soundness meets incompleteness in DQBF, Unnamed Item, Unnamed Item, The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1, CAQE and QuAbS: Abstraction Based QBF Solvers, Certified DQBF solving by definition extraction, DQBDD: an efficient BDD-based DQBF solver
Uses Software
