Transforming quantified Boolean formulas using biclique covers

DOI10.1007/978-3-031-30820-8_23MaRDI QIDQ6536143zbMATH OpenFDO

Authors Oliver Kullmann, Ankit Shukla

Publication date 5 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-30820-8_23

zbMATH Keywords

2QCNFbiclique cover problemconflict graphDQBFHorn clause setsminimal unsatisfiabilitypreprocessingQBF solving

Mathematics Subject Classification ID

Computational aspects of satisfiability (68R07) Graph theory (including graph drawing) in computer science (68R10)

Recommendations

• scientific article; zbMATH DE number 5719280
• From DQBF to QBF by dependency elimination
• Rewriting (dependency-)quantified 2-CNF with arbitrary free literals into existential 2-HORN
• Generalizations of matched CNF formulas
• Phase transition in matched formulas and a heuristic for biclique satisfiability

Cites work

• 2QBF: challenges and solutions
• An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF
• Bipartite dimensions and bipartite degrees of graphs
• Clausal abstraction for DQBF
• Covering graphs with few complete bipartite subgraphs
• Davis and Putnam meet Henkin: solving DQBF with resolution
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• Efficient approximation for restricted biclique cover problems
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 1432797 (Why is no real title available?)
• scientific article; zbMATH DE number 5493266 (Why is no real title available?)
• Incremental determinization
• On the Addressing Problem for Loop Switching
• On the parameterized complexity of biclique cover and partition
• Proof of the squashed cube conjecture
• sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning
• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• The biclique covering number of grids
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Understanding and extending incremental determinization for 2QBF

Cited in

(1)

• Compact representation of semilinear and terrain-like graphs

This page was built for publication: Transforming quantified Boolean formulas using biclique covers

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