Proving the infeasibility of Horn formulas through Read-once resolution. (English) Zbl 07868443
Summary: In this paper, we study Horn formulas from the perspective of read-once resolution refutations (RORs). A Horn formula is a Boolean formula in conjunctive normal form (CNF), in which each clause contains at most one positive literal. Horn formulas are used in a number of domains, including program verification, logic programming, and econometrics. In particular, deduction in ProLog is based on unification. Unification is based on resolution and instantiation. Resolution is a system used to prove the infeasibility of Boolean formulas. It is important to note that resolution is both sound and complete. However, resolution is inefficient in the following sense: There exist CNF formulas with resolution refutations whose lengths are bounded below by an exponential function of the input size. At the same time, these formulas admit shorter (polynomially bounded) proofs of infeasibility in other proof systems, such as Frege Systems. Despite this inefficiency, resolution is simple and easy to implement and hence used in a wide variety of theorem provers. In this paper, we study two variants of resolution. These are read-once resolution (ROR) and read-once unit resolution (UROR). Both ROR and UROR are sound. However, they are incomplete since there exist infeasible Boolean formulas which do not have either an ROR or a UROR. In this paper, we look at the problems of determining if a Horn formula has an ROR or a UROR. We also examine the problem of finding the optimal length ROR of a Horn formula from both the computational complexity and the approximation perspectives. Finally, we analyze the copy complexity of Horn formulas with respect to URORs.
References:
| [1] | Alan Robinson, J.; Voronkov, Andrei, Handbook of Automated Reasoning \((2\) Volume Set), 2001, MIT Press · Zbl 0964.00020 |
| [2] | Michael Alekhnovich, Alexander A. Razborov, Lower bounds for polynomial calculus: Non-binomial case, in: 42nd Annual Symposium on Foundations of Computer Science, FOCS 2001, 14-17 October 2001, Las Vegas, Nevada, USA, 2001, pp. 190-199. |
| [3] | Paul Beame, Russell Impagliazzo, Jan Krajícek, Toniann Pitassi, Pavel Pudlák, Lower bound on Hilbert’s Nullstellensatz and propositional proofs, in: 35th Annual Symposium on Foundations of Computer Science, Santa Fe, New Mexico, USA, 20-22 November 1994, 1994, pp. 794-806. · Zbl 0853.03017 |
| [4] | Beame, Paul; Pitassi, Toniann, Propositional proof complexity: Past, present, future, Bull. EATCS, 65, 66-89, 1998 · Zbl 0908.68164 |
| [5] | Bonet, Maria Luisa; Pitassi, Toniann; Raz, Ran, Lower bounds for cutting planes proofs with small coefficients, J. Symbolic Logic, 62, 3, 708-728, 1997 · Zbl 0889.03050 |
| [6] | Hans Kleine Büning, Piotr J. Wojciechowski, K. Subramani, Read-once resolutions in Horn formulas, in: Frontiers in Algorithmics - 13th International Workshop, FAW 2019, Sanya, China, April 29-May 3, 2019, Proceedings, 2019, pp. 100-110. · Zbl 1525.68196 |
| [7] | Büning, Hans Kleine; Wojciechowski, Piotr J.; Subramani, K., Finding read-once resolution refutations in systems of 2CNF clauses, Theoret. Comput. Sci., 729, 42-56, 2018 · Zbl 1435.03086 |
| [8] | Büning, Hans Kleine; Zhao, Xishun, The complexity of read-once resolution, Ann. Math. Artif. Intell., 36, 4, 419-435, 2002 · Zbl 1015.68081 |
| [9] | Samuel R. Buss, Propositional Proof Complexity: An Introduction. · Zbl 0946.68128 |
| [10] | Chandrasekaran, R.; Subramani, K., A combinatorial algorithm for horn programs, Discrete Optim., 10, 85-101, 2013 · Zbl 1284.90038 |
| [11] | Chvatal, V., Edmonds polytopes and a hierarchy of combinatorial problems, Discrete Math., 4, 10-11, 886-904, 1973 · Zbl 1106.05070 |
| [12] | Cook, W.; Coullard, C. R.; Turan, Gy., On the complexity of cutting-plane proofs, Discrete Appl. Math., 18, 25-38, 1987 · Zbl 0625.90056 |
| [13] | Stephen A. Cook, Robert A. Reckhow, On the lengths of proofs in the propositional calculus (preliminary version), in: Proceedings of the 6th Annual ACM Symposium on Theory of Computing, April 30-May 2, 1974, Seattle, Washington, USA, 1974, pp. 135-148. · Zbl 0375.02004 |
| [14] | Cormen, T. H.; Leiserson, C. E.; Rivest, R. L.; Stein, C., Introduction To Algorithms, 2001, MIT Press · Zbl 1047.68161 |
| [15] | Cousot, Patrick; Cousot, Radhia, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, (POPL, 1977), 238-252 |
| [16] | Davydov, Gennady; Davydova, Inna; Büning, Hans Kleine, An efficient algorithm for the minimal unsatisfiability problem for a subclass of CNF, Ann. Math. Artif. Intell., 23, 3-4, 229-245, 1998 · Zbl 0913.68090 |
| [17] | Dowling, William F.; Gallier, Jean H., Linear-time algorithms for testing the satisfiability of propositional horn formulae, J. Log. Program., 1, 3, 267-284, 1984 · Zbl 0593.68062 |
| [18] | Escoffier, Bruno; Paschos, Vangelis Th., Completeness in approximation classes beyond APX, Theoret. Comput. Sci., 359, 1, 369-377, 2006 · Zbl 1099.68135 |
| [19] | Gallier, Jean H., Logic for computer science: Foundations for automatic theorem proving, (Dover Books on Computer Science, 2015, Dover Publications) · Zbl 0605.03004 |
| [20] | Gomory, R. E., Outline of an algorithm for integer solutions to linear programs, Bull. Amer. Math. Soc., 64, 275-278, 1958 · Zbl 0085.35807 |
| [21] | Haken, A., The intractability of resolution, Theoret. Comput. Sci., 39, 2-3, 297-308, 1985 · Zbl 0586.03010 |
| [22] | Federico Heras, João Marques-Silva, Read-once resolution for unsatisfiability-based max-sat algorithms, in: IJCAI 2011, Proceedings of the 22nd International Joint Conference on Artificial Intelligence, Barcelona, Catalonia, Spain, July 16-22, 2011, 2011, pp. 572-577. |
| [23] | Russell Impagliazzo, Toniann Pitassi, Alasdair Urquhart, Upper and lower bounds for tree-like cutting planes proofs, in: Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS ’94), Paris, France, July 4-7, 1994, 1994, pp. 220-228. |
| [24] | Iwama, K.; Miyano, E., Intractability of read-once resolution, (Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC ’95), 1995, IEEE Computer Society Press: IEEE Computer Society Press Los Alamitos, CA, USA), 29-36 |
| [25] | Krajícek, Jan, Lower bounds to the size of constant-depth propositional proofs, J. Symbolic Logic, 59, 1, 73-86, 1994 · Zbl 0798.03056 |
| [26] | Liberatore, Paolo, Redundancy in logic II: 2CNF and horn propositional formulae, Artificial Intelligence, 172, 2, 265-299, 2008 · Zbl 1182.68282 |
| [27] | Orponen, Pekka; Mannila, Heikki, On approximation preserving reductions: Complete problems and robust measures, 1987, Department of Computer Science, University of Helsinki |
| [28] | Owre, Sam; Shankar, Natarajan, The formal semantics of PVS, 1999 · Zbl 1165.68468 |
| [29] | Papadimitriou, Christos H., Computational Complexity, 1994, Addison-Wesley: Addison-Wesley New York · Zbl 0833.68049 |
| [30] | Pudlák, Pavel, Lower bounds for resolution and cutting plane proofs and monotone computations, J. Symbolic Logic, 62, 3, 981-998, 1997 · Zbl 0945.03086 |
| [31] | Reckhow, Robert A., On the lengths of proofs in the propositional calculus, 1975, University of Toronto: University of Toronto Ontario, Canada, (Ph.D. thesis) |
| [32] | Robinson, John Alan, A machine-oriented logic based on the resolution principle, J. ACM, 12, 1, 23-41, 1965 · Zbl 0139.12303 |
| [33] | (Rudich, Steven; Wigderson, Avi, Computational Complexity Theory. Computational Complexity Theory, IAS / Park City mathematics series, vol. 10, 2004, AMS Chelsea Publishing) · Zbl 1048.68008 |
| [34] | Rushby, John M.; Owre, Sam; Shankar, Natarajan, Subtypes for specifications: Predicate subtyping in pvs, IEEE Trans. Software Eng., 24, 9, 709-720, 1998 |
| [35] | Segerlind, Nathan, The complexity of propositional proofs, Bull. Symbolic Logic, 13, 4, 417-481, 2007 · Zbl 1133.03037 |
| [36] | Stefan Szeider, NP-completeness of refutability by literal-once resolution, in: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, vol. 2083, 2001, pp. 168-181. · Zbl 0988.03020 |
| [37] | Tseitin, G. S., On the complexity of derivation in propositional calculus, (Siekmann, Jörg H.; Wrightson, Graham, Automation of Reasoning: 2: Classical Papers on Computational Logic 1967-1970, 1983, Springer Berlin Heidelberg: Springer Berlin Heidelberg Berlin, Heidelberg), 466-483 |
| [38] | Urquhart, Alasdair, The complexity of propositional proofs, Bull. Symbolic Logic, 1, 4, 425-467, 1995 · Zbl 0845.03025 |
| [39] | Wojciechowski, Piotr J.; Subramani, K., Copy complexity of horn formulas with respect to unit read-once resolution, Theoret. Comput. Sci., 890, 70-86, 2021 · Zbl 1514.68086 |
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.
