Document Open Access Logo

New Results on Cutting Plane Proofs for Horn Constraint Systems

Authors Hans Kleine Büning, Piotr Wojciechowski, K. Subramani

PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2019.43.pdf
  • Filesize: 467 kB
  • 14 pages

Document Identifiers

Author Details

Hans Kleine Büning
  • Universität Paderborn, Paderborn, Germany
Piotr Wojciechowski
  • LDCSEE, West Virginia University, Morgantown, WV, USA
K. Subramani
  • LDCSEE, West Virginia University, Morgantown, WV, USA

Funding

This research was supported in part by the Air-Force Office of Scientific Research through Grant FA9550-19-1-017.

Cite AsGet BibTex

Hans Kleine Büning, Piotr Wojciechowski, and K. Subramani. 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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 150, pp. 43:1-43:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.FSTTCS.2019.43

Abstract

In this paper, we investigate properties of cutting plane based refutations for a class of integer programs called Horn constraint systems (HCS). Briefly, a system of linear inequalities A * x >= b is called a Horn constraint system, if each entry in A belongs to the set {0,1,-1} and furthermore there is at most one positive entry per row. Our focus is on deriving refutations i.e., proofs of unsatisfiability of such programs using cutting planes as a proof system. We also look at several properties of these refutations. Horn constraint systems can be considered as a more general form of propositional Horn formulas, i.e., CNF formulas with at most one positive literal per clause. Cutting plane calculus (CP) is a well-known calculus for deciding the unsatisfiability of propositional CNF formulas and integer programs. Usually, CP consists of a pair of inference rules. These are called the addition rule (ADD) and the division rule (DIV). In this paper, we show that cutting plane calculus is still complete for Horn constraints when every intermediate constraint is required to be Horn. We also investigate the lengths of cutting plane proofs for Horn constraint systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • Horn constraints
  • cutting planes
  • proof length

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M. Alekhnovich, S. Buss, S. Moran, and T. Pitassi. Minimum Propositional Proof Length is NP-Hard to Linearly Approximate. In Mathematical Foundations of Computer Science (MFCS), pages 176-184. Springer-Verlag, 1998. Lecture Notes in Computer Science. Google Scholar
  2. Alexey Bakhirkin and David Monniaux. Combining Forward and Backward Abstract Interpretation of Horn Clauses. In Static Analysis - 24th International Symposium, SAS 2017, New York, NY, USA, August 30 - September 1, 2017, Proceedings, pages 23-45, 2017. Google Scholar
  3. Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan, and Andrey Rybalchenko. 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. Google Scholar
  4. Maria Luisa Bonet, Sam Buss, Alexey Ignatiev, Joao Marques-Silva, and Antonio Morgado. MaxSAT Resolution With the Dual Rail Encoding. In AAAI Conference on Artificial Intelligence, 2018. URL: https://www.aaai.org/ocs/index.php/AAAI/AAAI18/paper/view/16782/16235.
  5. Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. Lower Bounds for Cutting Planes Proofs with Small Coefficients. J. Symb. Log., 62(3):708-728, 1997. Google Scholar
  6. R. Chandrasekaran and K. Subramani. A combinatorial algorithm for Horn programs. Discrete Optimization, 10:85-101, 2013. Google Scholar
  7. Alessandro Cimatti, Alberto Griggio, and Roberto Sebastiani. Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories. J. Artif. Intell. Res. (JAIR), 40:701-728, 2011. Google Scholar
  8. W. Cook, C. R. Coullard, and Gy. Turan. On the complexity of Cutting-Plane Proofs. Discrete Applied Mathematics, 18:25-38, 1987. Google Scholar
  9. Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In POPL, pages 238-252, 1977. Google Scholar
  10. Marcel Dhiflaoui, Stefan Funke, Carsten Kwappik, Kurt Mehlhorn, Michael Seel, Elmar Schömer, Ralph Schulte, and Dennis Weber. Certifying and repairing solutions to large LPs how good are LP-solvers? In SODA, pages 255-256, 2003. Google Scholar
  11. Gyula Farkas. Über die Theorie der Einfachen Ungleichungen. Journal für die Reine und Angewandte Mathematik, 124(124):1-27, 1902. Google Scholar
  12. R. E. Gomory. Outline of an algorithm for integer solutions to linear programs. Bulletin of the American Mathematical Society, 64:275-278, 1958. Google Scholar
  13. A. Haken. The intractability of resolution. Theoretical Computer Science, 39(2-3):297-308, August 1985. Google Scholar
  14. John N. Hooker. Generalized Resolution and Cutting Planes. Annals of Operations Research, 12(1-4):217-239, 1988. Google Scholar
  15. K. Iwama and E. Miyano. 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. Google Scholar
  16. Joxan Jaffar and Michael Maher. Constraint Logic Programming: A Survey. The Journal of Logic Programming, s 19–20:503–581, October 1994. URL: https://doi.org/10.1016/0743-1066(94)90033-7.
  17. Haim Kaplan and Yahav Nussbaum. Certifying algorithms for recognizing proper circular-arc graphs and unit circular-arc graphs. Discrete Applied Mathematics, 157(15):3216-3230, 2009. Google Scholar
  18. Richard M. Karp. Reducibility among combinatorial problems. In R. E. Miller and J. W. Thatcher, editors, Complexity of Computer Computations, pages 85-103, New York, 1972. Plenum Press. Google Scholar
  19. Hans Kleine Büning, Piotr J. Wojciechowski, and K. Subramani. On the application of restricted cutting plane systems to Horn constraint systems. In The 12th International Symposium on Frontiers of Combining Systems, London, United Kingdom,, September 4-6, 2019, Proceedings, pages 149-164, 2019. Google Scholar
  20. Anvesh Komuravelli, Nikolaj Bjørner, Arie Gurfinkel, and Kenneth L. McMillan. Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. In Formal Methods in Computer-Aided Design, FMCAD 2015, Austin, Texas, USA, September 27-30, 2015., pages 89-96, 2015. Google Scholar
  21. Dieter Kratsch, Ross M. McConnell, Kurt Mehlhorn, and Jeremy Spinrad. Certifying algorithms for recognizing interval graphs and permutation graphs. In SODA, pages 158-167, 2003. Google Scholar
  22. Kung-Kiu Lau and Mario Ornaghi. Specifying Compositional Units for Correct Program Development in Computational Logic. In Program Development in Computational Logic: A Decade of Research Advances in Logic-Based Program Development, pages 1-29. Springer, 2004. Google Scholar
  23. R. M. McConnell, K. Mehlhorn, S. Näher, and P. Schweitzer. Certifying algorithms. Computer Science Review, 5(2):119-161, 2011. Google Scholar
  24. Microsoft Research. Z3: An efficient SMT solver. URL: http://research.microsoft.com/projects/z3/.
  25. G. L. Nemhauser and L. A. Wolsey. Integer and Combinatorial Optimization. John Wiley & Sons, New York, 1999. Google Scholar
  26. Pavel Pudlák. Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations. J. Symb. Log., 62(3):981-998, 1997. URL: https://doi.org/10.2307/2275583.
  27. A. Schrijver. Theory of Linear and Integer Programming. John Wiley and Sons, New York, 1987. Google Scholar
  28. SRI International. Yices: An SMT solver. URL: http://yices.csl.sri.com/.
  29. K. Subramani. Optimal Length Resolution Refutations of Difference Constraint Systems. Journal of Automated Reasoning (JAR), 43(2):121-137, 2009. Google Scholar
  30. K. Subramani and Piotr Wojciechowki. A Polynomial Time Algorithm for Read-Once Certification of Linear Infeasibility in UTVPI Constraints. Algorithmica, 81(7):2765-2794, 2019. Google Scholar
  31. 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, pages 168-181, 2001. Google Scholar
  32. A.F. Veinott and G.B. Dantzig. Integral Extreme points. SIAM Review, 10:371-372, 1968. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact