@inproceedings{58d2949377fa48b88f74a12a19c93052,
title = "Transforming Quantified Boolean Formulas Using Biclique Covers",
abstract = "We introduce the global conflict graph of DQCNFs (dependency quantified conjunctive normal forms), recording clashes between clauses on such universal variables on which all existential variables depend (called “global variables”). The biclique covers of this graph correspond to the eligible clause-slices of the DQCNF which consider only the global variables. We show that all such slices yield satisfiability-equivalent variations. This opens the possibility to realise this slice using as few global variables as possible. We give basic theoretical results and first supporting experimental data.",
author = "Oliver Kullmann and Ankit Shukla",
year = "2023",
month = apr,
language = "English",
volume = "13994",
series = "Lecture Notes in Computer Science (LNCS)",
publisher = "Springer",
pages = "372–390",
editor = "\{Sriram Sankaranarayanan, Natasha Sharygina\}",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, \{TACAS\} 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, \{ETAPS",
}