TL;DR
This paper discusses developing advanced reasoning tools for DQBF by exploiting properties like autarkies and symmetries to improve solver efficiency and robustness.
Contribution
It introduces the potential use of autarkies and symmetries for pre- and in-processing in DQBF solving, extending techniques from SAT and QBF.
Findings
Identification of autarkies and symmetries as exploitable properties
Development of automated testing and debugging techniques for DQBF
Ongoing development of a DQBF solver tool
Abstract
The aim of this PhD project is to develop fast and robust reasoning tools for dependency quantified Boolean formulas (DQBF). In this paper, we outline two properties, autarkies and symmetries, that potentially can be exploited for pre- and in-processing in the DQBF solving process. DQBF extend quantified Boolean formulas (QBF) with non-linear dependencies between the quantified variables. Automated testing and debugging techniques are an essential part of the solvers tool-chain. For rigorous DQBF solver development, we are working on novel automated testing and debugging techniques as successfully established in SAT and QBF solving. The tool is under development.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Testing and Debugging Techniques · Logic, programming, and type systems