Incremental Determinization

DOI10.1007/978-3-319-40970-2_23zbMath1475.68222OpenAlexW4235759561MaRDI QIDQ2818028

Sanjit A. Seshia, Markus N. Rabe

Publication date: 5 September 2016

Published in: Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL: https://escholarship.org/uc/item/67x817fp

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational aspects of satisfiability (68R07)

Related Items (8)

Functional synthesis via input-output separation ⋮ Boolean functional synthesis: from under the hood of solvers ⋮ Encodings of Bounded Synthesis ⋮ Boolean functional synthesis: hardness and practical algorithms ⋮ The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17) ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers ⋮ Davis and Putnam meet Henkin: solving DQBF with resolution ⋮ Certified DQBF solving by definition extraction

Uses Software

• PicoSAT
• Bloqqer
• Nenofex
• QBFLIB
• DepQBF
• CAQE
• Quantor
• sKizzo
• RAReQS
• QESTO

Cites Work

• Unnamed Item
• Unnamed Item
• On the power of clause-learning SAT solvers as resolution engines
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Efficiently solving quantified bit-vector formulas
• Solving QBF with Counterexample Guided Refinement
• On QBF Proofs and Preprocessing
• On Unification of QBF Resolution-Based Calculi
• Abstraction-Based Algorithm for 2QBF
• Fast DQBF Refutation
• A Unified Proof System for QBF Preprocessing
• Nenofex: Expanding NNF for QBF Solving
• Ranking Function Synthesis for Bit-Vector Relations
• A Non-prenex, Non-clausal QBF Solver with Game-State Learning
• Blocked Clause Elimination for QBF
• Recovering and Utilizing Partial Duality in QBF
• Experiments with Reduction Finding
• Automated Deduction – CADE-20
• A Machine-Oriented Logic Based on the Resolution Principle
• A machine program for theorem-proving
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency

This page was built for publication: Incremental Determinization