Document

# New Results on Cutting Plane Proofs for Horn Constraint Systems

## File

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

## Cite As

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

## 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.
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.
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.
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.
6. R. Chandrasekaran and K. Subramani. A combinatorial algorithm for Horn programs. Discrete Optimization, 10:85-101, 2013.
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.
8. W. Cook, C. R. Coullard, and Gy. Turan. On the complexity of Cutting-Plane Proofs. Discrete Applied Mathematics, 18:25-38, 1987.
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.
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.
11. Gyula Farkas. Über die Theorie der Einfachen Ungleichungen. Journal für die Reine und Angewandte Mathematik, 124(124):1-27, 1902.
12. R. E. Gomory. Outline of an algorithm for integer solutions to linear programs. Bulletin of the American Mathematical Society, 64:275-278, 1958.
13. A. Haken. The intractability of resolution. Theoretical Computer Science, 39(2-3):297-308, August 1985.
14. John N. Hooker. Generalized Resolution and Cutting Planes. Annals of Operations Research, 12(1-4):217-239, 1988.
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.
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.
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.
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.
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.
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.
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.
23. R. M. McConnell, K. Mehlhorn, S. Näher, and P. Schweitzer. Certifying algorithms. Computer Science Review, 5(2):119-161, 2011.
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.
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.
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.
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.
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.
32. A.F. Veinott and G.B. Dantzig. Integral Extreme points. SIAM Review, 10:371-372, 1968.
X

Feedback for Dagstuhl Publishing