Peitl, T., Slivovsky, F., & Szeider, S. (2016). Long Distance Q-Resolution with Dependency Schemes. In N. Creignou & D. Le Berre (Eds.), Theory and Applications of Satisfiability Testing – SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings. Cham. https://doi.org/10.1007/978-3-319-40970-2_31
Resolution proof systems for quantified Boolean formulas (QBFs) provide a formal model for studying the limitations of state-of-the-art search-based QBF solvers, which use these systems to generate proofs. In this paper, we define a new proof system that combines two such proof systems: Q-resolution with generalized universal reduction according to a dependency scheme and long distance Q-resolution. We show that the resulting proof system is sound for the reflexive resolution-path dependency scheme—in fact, we prove that it admits strategy extraction in polynomial time. As a special case, we obtain soundness and polynomial-time strategy extraction for long distance Q-resolution with universal reduction according to the standard dependency scheme. We report on experiments with a configuration of DepQBF that generates proofs in this system.
en
Additional information:
The final publication is available via <a href="https://doi.org/10.1007/978-3-319-40970-2_31" target="_blank">https://doi.org/10.1007/978-3-319-40970-2_31</a>.
