Title: A Combinatorial Characterization of Treelike Resolution Space
Abstract:We show that the Player-Adversary game of Pudlak and Impagliazzo [A lower bound for DLL algorithms for k-SAT, in: Proc. 11th Annual ACM-SIAM Symposium on Discrete Algorithms, 2000, pp. 128-136] played...We show that the Player-Adversary game of Pudlak and Impagliazzo [A lower bound for DLL algorithms for k-SAT, in: Proc. 11th Annual ACM-SIAM Symposium on Discrete Algorithms, 2000, pp. 128-136] played over CNF propositional formulas gives an exact characterization of the space needed in treelike resolution refutations. This characterization is purely combinatorial and independent of the notion of resolution. We use this characterization to give for the first time a separation between the space needed in treelike and general resolution.Read More
Publication Year: 2003
Publication Date: 2003-01-01
Language: en
Type: article
Access and Citation
Cited By Count: 2
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot