Oliver Kullmann, Ankit Shukla,
"Transforming Quantified Boolean Formulas Using Biclique Covers"
, in Sriram Sankaranarayanan, Natasha Sharygina: 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, Serie Lecture Notes in Computer Science (LNCS), Vol. 13994, Springer, Seite(n) 372?390, 4-2023
Original Titel:
Transforming Quantified Boolean Formulas Using Biclique Covers
Sprache des Titels:
Englisch
Original Buchtitel:
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
Original Kurzfassung:
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.
Forschungs-