Understanding and extending incremental determinization for 2QBF

DOI10.1007/978-3-319-96142-2_17MaRDI QIDQ6039407zbMATH OpenOpenAlexFDO

Authors Markus Rabe, Leander Tentrup, Cameron Rasmussen, Sanjit A. Seshia

Publication date 5 May 2023

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1905.13411, https://escholarship.org/uc/item/62j6b4gj

Mathematics Subject Classification ID

Logic in computer science (03B70) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: Incremental determinization is a recently proposed algorithm for solving quantified Boolean formulas with one quantifier alternation. In this paper, we formalize incremental determinization as a set of inference rules to help understand the design space of similar algorithms. We then present additional inference rules that extend incremental determinization in two ways. The first extension integrates the popular CEGAR principle and the second extension allows us to analyze different cases in isolation. The experimental evaluation demonstrates that the extensions significantly improve the performance.

Recommendations

• Incremental QBF solving by DepQBF
• Abstraction-based algorithm for 2QBF
• Verification of partial designs using incremental QBF
• Incremental determinization
• Dynamic QBF dependencies in reduction and expansion
• Formal Methods in Computer-Aided Design
• Expansion-based QBF solving versus Q-resolution

Cited in

(6)

• Boolean functional synthesis: hardness and practical algorithms
• Incremental determinization
• CAQE and QuAbS: Abstraction Based QBF Solvers
• Incremental determinization for quantifier elimination and functional synthesis
• Transforming quantified Boolean formulas using biclique covers
• Hashing-based approximate counting of minimal unsatisfiable subsets

This page was built for publication: Understanding and extending incremental determinization for 2QBF

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6039407)