Information Technology Reference
In-Depth Information
[BW01] E. Ben-Sasson, A. Wigderson, Short proofs are narrow—resolution made simple.
J. ACM
48
(2), 149-169 (2001)
[Bey11] O. Beyersdorff, in
Proofs and Games
. Lecture notes 2011,
http://www.thi.uni-
[BGL10] O. Beyersdorff, N. Galesi, M. Lauria, A lower bound for the pigeon hole principle
in tree-like resolution by asymmetric prover-delayer games. Inf. Process. Lett.
110
,
1074-1077 (2010)
[BGL11] O. Beyersdorff, N. Galesi, M. Lauria, Parameterized complexity of DPLL search pro-
cedures, in
Proceedings of 14th Conference on Theory and Applications of Satisfiability
Testing
, LNCS, vol. 6695, pp. 5-18, 110 (2011)
[BGL13] O. Beyersdorff, N. Galesi, M. Lauria, A characterization of tree-like resolution size.
Inf. Process. Lett.
113
, 666-671 (2013)
[BEGJ02] M.L. Bonet, J.L. Esteban, N. Galesi, J. Johannsen, On the relative complexity of
resolution refinements and cutting planes proof systems. SIAM J. Comput.
30
(5),
1462-1484 (2002)
[BP97]
S. Buss, T. Pitassi, Resolution and the weak pigeonhole principle, in
Proceedings of
Computer Science Logic 97
, Springer Verlag. LNCS, vol. 1414, pp. 149-156 (1997)
[CS88]
V. Chvátal, E. Szemerédi, Many hard examples for resolution. J. ACM
35
, 759-768
(1988)
[DR01]
S. Dantchev, S. Riis, Tree resolution proofs and the weak pigeon hole principle, in
Proceedings of 16th IEEE Conference on Computational Complexity
, pp. 69-75 (2001)
[ET01]
J.L. Esteban, J. Torán, Space bounds for resolution. Inf. Comput.
171
(1), 84-97 (2001)
[ET03]
J.L. Esteban, J. Torán, Combinatorial characterization of tree-like resolution space.
Inf. Process. Lett.
87
(6), 295-300 (2003)
[Hak85]
A. Haken, The intractability of resolution. Theoret. Comput. Sci.
39
(2-3), 297-308
(1985)
[HU07]
A. Hertel, A. Urquhart, Game characterizations and the PSPACE-completeness of tree
resolution space, in
Proceedings of CSL 2007
, pp. 527-541 (2007)
[IM99]
K. Iwama, S. Miyazaki, Tree-like resolution is superpolynomially slower than dag-like
resolution, in
Proceedings of 10th ISAAC
, LNCS, vol. 1741, pp. 133-142 (1999)
[Nor12]
J. Nordström, Personal communication (2012)
[PI00]
P. Pudlák, R. Impagliazzo, A lower bound for DLL algorithms for
k
-SAT, in
Pro-
ceedings of 11th Annual ACM-SIAM Symposium on Discrete Algorithms
, pp. 128-136
(2000)
[Rob65]
J.A. Robinson, A machine oriented logic based on the resolution principle. J. ACM
12
(1), 23-41 (1965)
[ST13]
U. Schöning, J. Torán,
The Satisfiability Problem SAT, Algorithms and Analyses
(Lehmanns media, Berlin, 2013)
[Tor99]
J. Torán, Lower bounds for the space used in resolution, in
Proceedings of 13th Com-
puter Science Logic Conference, Springer
. Lecture Notes in Computer Science, vol.
1683, pp. 362-373 (1999)
[Urq87]
A. Urquhart, Hard examples for resolution. J. ACM
34
, 209-219 (1987)
