The NP-hardness of finding a directed acyclic graph for regular resolution. (English) Zbl 1145.03034
Summary: Let \(R\) be a resolution refutation, given as a sequence of clauses without explicit description of the underlying dag. Then, it is NP-complete to decide whether \(R\) is a regular resolution refutation.
MSC:
| 03F20 | Complexity of proofs |
| 68Q17 | Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) |
References:
| [1] | Alekhnovich, M.; Buss, S.; Moran, S.; Pitassi, T., Minimum propositional proof length is NP-hard to linearly approximate, Journal of Symbolic Logic, 66, 171-191 (2001), An extended abstract appeared in Mathematical Foundations of Computer Science, MFCS’98, Springer-Verlag Lecture Notes in Computer Science, vol. 1450, 1998, pp. 176-184 · Zbl 0977.03032 |
| [2] | M. Alekhnovich, J. Johannsen, T. Pitassi, A. Urquhart, An exponential separation between regular and general resolution, in: Proc. 34th Annual ACM Symposium on Theory of Computing, 2002, pp. 448-456; M. Alekhnovich, J. Johannsen, T. Pitassi, A. Urquhart, An exponential separation between regular and general resolution, in: Proc. 34th Annual ACM Symposium on Theory of Computing, 2002, pp. 448-456 · Zbl 1192.03039 |
| [3] | M. Alekhnovich, A.A. Razborov, Resolution is not automatizable unless \(W [ P ]\); M. Alekhnovich, A.A. Razborov, Resolution is not automatizable unless \(W [ P ]\) · Zbl 1169.03044 |
| [4] | Bonet, M. L.; Esteban, J. L.; Galesi, N.; Johannsen, J., On the relative complexity of resolution refinements and cutting planes systems, SIAM Journal on Computing, 30, 1462-1484 (2000) · Zbl 0976.03062 |
| [5] | Cook, S. A.; Reckhow, R. A., The relative efficiency of propositional proof systems, Journal of Symbolic Logic, 44, 36-50 (1979) · Zbl 0408.03044 |
| [6] | Galil, Z., On the complexity of regular resolution and the David-Putnam procedure, Theoretical Computer Science, 4, 23-46 (1977) · Zbl 0385.68048 |
| [7] | Goerdt, A., Regular resolution versus unrestricted resolution, SIAM Journal on Computing, 22, 661-683 (1993) · Zbl 0781.68099 |
| [8] | Iwama, K., Complexity of finding short resolution proofs, (Prívara, I.; Ruzicka, P., Mathematical Foundations of Computer Science 1997. Mathematical Foundations of Computer Science 1997, Lecture Notes in Computer Science, vol. 1295 (1997), Springer-Verlag), 309-318 · Zbl 0935.03067 |
| [9] | Iwama, K.; Miyano, E., Intractability of read-once resolution, (Proceedings of the Tenth Annual Conference on Structure in Complexity Theory (1995), IEEE Computer Society: IEEE Computer Society Los Alamitos, California), 29-36 |
| [10] | T. Pitassi, R. Raz, Regular resolution lower bounds for the weak pigeonhole principle, in: Proc. 33rd Annual ACM Symposium on Theory of Computing, 2001, pp. 347-355; T. Pitassi, R. Raz, Regular resolution lower bounds for the weak pigeonhole principle, in: Proc. 33rd Annual ACM Symposium on Theory of Computing, 2001, pp. 347-355 · Zbl 1323.03090 |
| [11] | Siekmann, J.; Wrightson, G., Automation of Reasoning, vol. 1-2 (1983), Springer-Verlag: Springer-Verlag Berlin · Zbl 0567.03001 |
| [12] | Szeider, S., NP-completeness of refutability by literal-once resolution, (Automated Reasoning: First International Joint Conference. Automated Reasoning: First International Joint Conference, IJCAR (2001), Springer Verlag), 168-181 · Zbl 0988.03020 |
| [13] | Tsejtin, G. S., On the complexity of derivation in propositional logic, Studies in Constructive Mathematics and Mathematical Logic, 2, 115-125 (1968), Reprinted in [11, vol 2], pp. 466-483 · Zbl 0205.00402 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
