Abstract
In this paper, we analyze the copy complexity of unsatisfiable Horn constraint systems, under the ADD refutation system. Recall that a linear constraint of the form \(\sum _{i=1}^{n} a_{i}\cdot x_{i} \ge b\), is said to be a horn constraint if all the \(a_{i} \in \{0,1,-1\}\) and at most one of the \(a_{i}\)s is positive. A conjunction of such constraints is called a Horn constraint system (HCS). Horn constraints arise in a number of domains including, but not limited to, program verification, power systems, econometrics, and operations research. The ADD refutation system is both sound and complete. Additionally, it is the simplest and most natural refutation system for refuting the feasibility of a system of linear constraints. The copy complexity of an infeasible linear constraint system (not necessarily Horn) in a refutation system, is the minimum number of times each constraint needs to be replicated, in order to obtain a read-once refutation. We show that for an HCS with n variables and m constraints, the copy complexity is at most \(2^{n-1}\), in the ADD refutation system. Additionally, we analyze bounded-width HCSs from the perspective of copy complexity. Finally, we provide an empirical analysis of an integer programming formulation of the copy complexity problem in HCSs. (An extended abstract was published in FroCos 2021 [26].)
Similar content being viewed by others
References
Bakhirkin, A., Monniaux, D.: Combining forward and backward abstract interpretation of Horn clauses. Static Analysis - 24th International Symposium, SAS 2017, New York, USA, August 30 - September 1, 2017, Proceedings, pages 23–45 (2017)
Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, pages 24–51 (2015)
Chandrasekaran, R., Subramani, K.: A combinatorial algorithm for Horn programs. Discrete Optimization 10, 85–101 (2013)
De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Verimap: a tool for verifying programs through transformations. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 568–574. Springer (2014)
De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. Microsoft Research (2008). http://research.microsoft.com/projects/z3/
Farkas, G.: Über die Theorie der Einfachen Ungleichungen. J. für die Reine und Angewandte Mathematik, 124(124), 1–27 (1902)
Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Solving constrained horn clauses using syntax and data. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pages 1–9. IEEE, (2018)
Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. ACM SIGPLAN Notices 47(6), 405–416 (2012)
Hojjat, H., Rümmer, P.: The Eldarica Horn solver. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pages 1–7. IEEE, (2018)
Iwama, K., Miyano, E.: Intractability of read-once resolution. In: Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC ’95), pages 29–36, Los Alamitos, CA, USA, June 1995. IEEE Computer Society Press
Kafle, B., Gallagher, J.P., Morales, J.F.: Rahft: a tool for verifying Horn clauses using abstract interpretation and finite tree automata. In: International Conference on Computer Aided Verification, pages 261–268. Springer, (2016)
Karp, R.M.: Reducibility among combinatorial problems. In: Miller, R. E., Thatcher, J. W. (eds.), Complexity of Computer Computations, pages 85–103, New York, 1972. Plenum Press
Kleine Büning, H., Wojciechowski, P., Chandrasekaran, R. and Subramani, K.: Restricted cutting plane proofs in Horn constraint systems. In: Herzig, A., Popescu, A. (eds.), Frontiers of Combining Systems - 12th International Symposium, FroCoS 2019, London, UK, September 4-6, 2019, Proceedings, vol. 11715 of Lecture Notes in Computer Science, pages 149–164. Springer (2019)
Büning, H.K., Wojciechowski, P., Subramani, K.: Finding read-once resolution refutations in systems of 2CNF clauses. Theor. Comput. Sci. 729, 42–56 (2018)
Büning, HK., Wojciechowski, P., Subramani, K.: New results on cutting plane proofs for Horn constraint systems. In: 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2019, December 11-13, 2019, Bombay, India, pages 43:1–43:14 (2019)
Büning, HK., Wojciechowski, P., Subramani, K.: Read-once resolutions in Horn formulas.In: Frontiers in Algorithmics - 13th International Workshop, FAW 2019, Sanya, China, April 29 - May 3, 2019, Proceedings, pages 100–110 (2019)
Komuravelli, A., Gurfinkel, A., Chaki, S.: Smt-based model checking for recursive programs. Formal Methods in System Design 48(3), 175–205 (2016)
LiCalzi, M., Veinott, A.F.: Subextremal functions and lattice programming. SSRN Electronic J., 10 2005
Wolsey, L.A., Nemhauser, G.L.: Integer and Combinatorial Optimization. John Wiley & Sons, New York (1999)
Orponen, P., Mannila, H.: On approximation preserving reductions: complete problems and robust measures. Technical report, Department of Computer Science, University of Helsinki (1987)
Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)
Schrijver, A.: Theory of Linear and Integer Programming. John Wiley and Sons, New York (1987)
Subramani, K.: Optimal length resolution refutations of difference constraint systems. J. Auto. Reas. (JAR) 43(2), 121–137 (2009)
Subramani, K., Wojciechowki, P.: A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints. Algorithmica 81(7), 2765–2794 (2019)
Subramani, K., Wojciechowki, P.: A combinatorial certifying algorithm for linear feasibility in UTVPI constraints. Algorithmica 78(1), 166–208 (2017)
Subramani, K., Wojciechowski, P., Velasquez, A.: On the copy complexity of width 3 Horn constraint systems. In: Konev, B., Reger, G. (eds.) editors, Frontiers of Combining Systems - 13th International Symposium, FroCoS 2021, Birmingham, UK, September 8-10, 2021, Proceedings, vol. 12941 of Lecture Notes in Computer Science, pages 63–78. Springer (2021)
Wojciechowski, P., Subramani, K.: Copy complexity of Horn formulas with respect to unit read-once resolution. Theor. Comput. Sci. 890, 70–86 (2021)
Author information
Authors and Affiliations
Contributions
All authors contributed equally.
Corresponding author
Ethics declarations
Competing interests
The authors declare no competing interests.
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
This research was supported in part by the Defense Advanced Research Projects Agency through grant HR001123S0001-FP-004.
Rights and permissions
Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
About this article
Cite this article
Subramani, K., Wojciechowki, P. & Velasquez, A. Farkas Bounds on Horn Constraint Systems. Theory Comput Syst 68, 227–249 (2024). https://doi.org/10.1007/s00224-023-10156-6
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00224-023-10156-6