Improving Reasoning on DQBF
Logic in Computer Science
2019-10-04 v1
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.
Cite
@article{arxiv.1910.01181,
title = {Improving Reasoning on DQBF},
author = {Ankit Shukla},
journal= {arXiv preprint arXiv:1910.01181},
year = {2019}
}
Comments
FMCAD'19 Student Forum