A certifying algorithm for lattice point feasibility in a system of UTVPI constraints.

*(English)*Zbl 1394.90499Summary: This paper is concerned with the design and analysis of a certifying algorithm for checking the lattice point feasibility of a class of constraints called unit two variable per inequality (UTVPI) constraints. A UTVPI constraint has at most two non-zero variables and the coefficients of the non-zero variables belong to the set \(\{+1,-1\}\). These constraints occur in a number of application domains, including but not limited to program verification, abstract interpretation, and operations research. As per the literature, the fastest known model generating algorithm for checking lattice point feasibility in UTVPI constraint systems runs in \(O(m\cdot n+n^2\cdot \log n)\) time and \(O(n^2)\) space, where \(m\) represents the number of constraints and \(n\) represents the number of variables in the constraint system [S. K. Lahiri and M. Musuvathi, Lect. Notes Comput. Sci. 3717, 168–183 (2005; Zbl 1171.68715)]. In this paper, we design and analyze a new algorithm for checking the lattice point feasibility of UTVPI constraints. The presented algorithm runs in \(O(m\cdot n)\) time and \(O(m+n)\) space. Additionally it is certifying in that it produces a satisfying assignment in the event that it is presented with feasible instances and refutations in the event that it is presented with infeasible instances. The importance of providing certificates cannot be overemphasized, especially in mission-critical applications. Our approaches for the lattice point feasibility problem in UTVPI constraint systems is fundamentally different from existing approaches for this problem; indeed, it is based on new insights into combining well-known inference rules for these systems.

##### MSC:

90C27 | Combinatorial optimization |

##### Software:

LEDA
PDF
BibTeX
XML
Cite

\textit{K. Subramani} and \textit{P. Wojciechowski}, J. Comb. Optim. 35, No. 2, 389--408 (2018; Zbl 1394.90499)

Full Text:
DOI

##### References:

[1] | Bagnara R, Hill P M, Zaffanella E (2008) An improved tight closure algorithm for integer octagonal constraints. In: VMCAI, pp 8-21 · Zbl 1138.68474 |

[2] | Cherkassky, BV; Goldberg, AV; Radzik, T, Shortest paths algorithms: theory and experimental evaluation, Math Program, 73, 129-174, (1996) · Zbl 0853.90111 |

[3] | Cormen TH, Leiserson CE, Rivest RL, Stein C (2001) Introduction to algorithms. MIT Press, Cambridge · Zbl 1047.68161 |

[4] | Cousot P, Cousot R (1977) Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM symposium on the principles of programming languages (POPL), ACM Press, pp 238-252 |

[5] | Dantzig GB, Eaves BC (1973) Fourier-Motzkin elimination and its dual. J Comb Theory (A) 14:288-297 · Zbl 0258.15010 |

[6] | Fouilhe A, Monniaux D, Périn M (2013). Efficient generation of correctness certificates for the abstract domain of polyhedra. In: Static analysis: 20th international symposium, pp 345-365 · Zbl 1073.68081 |

[7] | Gerber, R; Pugh, W; Saksena, M, Parametric dispatching of hard real-time tasks, IEEE Trans Comput, 44, 471-479, (1995) · Zbl 1062.68543 |

[8] | Haken, A, The intractability of resolution, Theor Comput Sci, 39, 297-308, (1985) · Zbl 0586.03010 |

[9] | Harvey W, Stuckey PJ (1997). A unit two variable per inequality integer constraint solver for constraint logic programming. In: Proceedings of the 20th Australasian computer science conference, pp 102-111 · Zbl 0586.03010 |

[10] | Hochbaum, DS; Naor, J, Simple and fast algorithms for linear and integer programs with two variables per inequality, SIAM J Comput, 23, 1179-1192, (1994) · Zbl 0831.90089 |

[11] | Jaffar J, Maher MJ, Stuckey PJ, Yap HC (1994) Beyond finite domains. In: Proceedings of the second international workshop on principles and practice of constraint programming (PPCP), lecture notes in computer science, vol 874, pp 86-94 · Zbl 1062.68543 |

[12] | Lahiri SK, Musuvathi M (2005) An Efficient decision procedure for UTVPI constraints. In: Proceedings of the \(5{\rm th}\) international workshop on the frontiers of combining systems (FroCos), lecture notes in computer science, vol 3717, pp 168-183 · Zbl 1171.68715 |

[13] | Mehlhorn K, Näher S (1999) The LEDA platform of combinatorial and geometric computing. Cambridge University Press, Cambridge · Zbl 0976.68156 |

[14] | Miné, A, The octagon abstract domain, High Order Symb Comput, 19, 31-100, (2006) · Zbl 1105.68069 |

[15] | Nieuwenhuis R, Oliveras A (2005) DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Proceedings of the \(17{\rm th}\) international conference on computer aided verification (CAV), lecture notes in computer science, vol 3576, pp 321-334 · Zbl 1081.68629 |

[16] | Nieuwenhuis R, Oliveras A, Tinelli C (2004) Abstract DPLL and abstract DPLL modulo theories. In: Proceedings of the \(11{\rm th}\) international conference on logic for programming, artificial intelligence and reasoning (LPAR), lecture notes in computer science, vol 3452, pp 36-50 · Zbl 1109.68097 |

[17] | Revesz PZ (2009) Tightened transitive closure of integer addition constraints. In: Proceedings of the \(8{\rm th}\) symposium on abstraction, reformulation and approximation (SARA), AAAI |

[18] | Schutt, A; Stuckey, PJ, Incremental satisfiability and implication for UTVPI constraints, INFORMS J Comput, 22, 514-527, (2010) · Zbl 1243.90141 |

[19] | Sitzmann I, Stuckey PJ (2000) O-trees: a constraint-based index structure. In: Australasian database conference, pp 127-134 |

[20] | Subramani, K, On deciding the non-emptiness of 2SAT polytopes with respect to first order queries, Math Logic Q, 50, 281-292, (2004) · Zbl 1073.68081 |

[21] | Subramani K, Wojciechowski P (2016) A combinatorial certifying algorithm for linear feasibility in UTVPI constraints. Algorithmica, First online: 28 April 2016 · Zbl 1360.68889 |

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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.