Nothing Special   »   [go: up one dir, main page]
Skip to main content
SpringerLink
Log in

Farkas Bounds on Horn Constraint Systems

  • Published:
Theory of Computing Systems Aims and scope Submit manuscript

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].)

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. 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)

  2. 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)

  3. Chandrasekaran, R., Subramani, K.: A combinatorial algorithm for Horn programs. Discrete Optimization 10, 85–101 (2013)

    Article  MathSciNet  Google Scholar 

  4. 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)

  5. De Moura, L., Bjørner, N.: Z3: An efficient SMT solver. Microsoft Research (2008). http://research.microsoft.com/projects/z3/

  6. Farkas, G.: Über die Theorie der Einfachen Ungleichungen. J. für die Reine und Angewandte Mathematik, 124(124), 1–27 (1902)

  7. 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)

  8. Grebenshchikov, S., Lopes, N.P., Popeea, C., Rybalchenko, A.: Synthesizing software verifiers from proof rules. ACM SIGPLAN Notices 47(6), 405–416 (2012)

    Article  Google Scholar 

  9. Hojjat, H., Rümmer, P.: The Eldarica Horn solver. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pages 1–7. IEEE, (2018)

  10. 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

  11. 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)

  12. 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

  13. 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)

  14. 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)

    Article  MathSciNet  Google Scholar 

  15. 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)

  16. 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)

  17. Komuravelli, A., Gurfinkel, A., Chaki, S.: Smt-based model checking for recursive programs. Formal Methods in System Design 48(3), 175–205 (2016)

    Article  Google Scholar 

  18. LiCalzi, M., Veinott, A.F.: Subextremal functions and lattice programming. SSRN Electronic J., 10 2005

  19. Wolsey, L.A., Nemhauser, G.L.: Integer and Combinatorial Optimization. John Wiley & Sons, New York (1999)

    Google Scholar 

  20. Orponen, P., Mannila, H.: On approximation preserving reductions: complete problems and robust measures. Technical report, Department of Computer Science, University of Helsinki (1987)

  21. Robinson, J.A.: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)

    Article  MathSciNet  Google Scholar 

  22. Schrijver, A.: Theory of Linear and Integer Programming. John Wiley and Sons, New York (1987)

    Google Scholar 

  23. Subramani, K.: Optimal length resolution refutations of difference constraint systems. J. Auto. Reas. (JAR) 43(2), 121–137 (2009)

    Article  MathSciNet  Google Scholar 

  24. Subramani, K., Wojciechowki, P.: A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints. Algorithmica 81(7), 2765–2794 (2019)

    Article  MathSciNet  Google Scholar 

  25. Subramani, K., Wojciechowki, P.: A combinatorial certifying algorithm for linear feasibility in UTVPI constraints. Algorithmica 78(1), 166–208 (2017)

    Article  MathSciNet  Google Scholar 

  26. 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)

  27. Wojciechowski, P., Subramani, K.: Copy complexity of Horn formulas with respect to unit read-once resolution. Theor. Comput. Sci. 890, 70–86 (2021)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LDCSEE, West Virginia University, Morgantown, WV, 26506, USA

    K. Subramani & Piotr Wojciechowki

  2. Department of Computer Science, University of Colorado at Boulder, Boulder, CO, 80309, USA

    Alvaro Velasquez

Authors
  1. K. Subramani
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Piotr Wojciechowki
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alvaro Velasquez
    View author publications

    You can also search for this author in PubMed Google Scholar

Contributions

All authors contributed equally.

Corresponding author

Correspondence to K. Subramani.

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.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

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

Download citation

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00224-023-10156-6

Keywords

Search

Navigation