Abstract
In this paper, we investigate the refutability of Difference Constraint Systems (DCSs) in the Unit Read-once Refutation (UROR) system. Recall that a difference constraint is a linear relationship of the form: \(x_{i}-x_{j} \le b_{ij}\) and a DCS is a conjunction of such constraints. DCSs arise in a number of application domains such as program verification and scheduling. It follows that efficient refutation methodologies for these systems are of paramount interest. The UROR system is incomplete, in that unsatisfiable difference constraint systems may not have a refutation in this system. However, this refutation system provides a useful tool for proving if a DCS is infeasible because of a restriction on the values the variables can take. Note that without any absolute constraints, the values of the variable in a solution to a DCS can be uniformly increased or decreased without changing the validity of the solution. Thus, the UROR refutations of a DCS depend upon the restrictions placed on the values variables can take. This is in contrast to unrestricted refutations, which need not depend on these restrictions. Investigating weak (incomplete) refutation systems leads to a better understanding of the inference rules required for establishing the infeasibility of the given constraint system.
This research was supported in part by the Air-Force Research Laboratory, Rome through Contract FA8750-17-S-7007 and in part by the Air-Force Office of Scientific Research through Grant FA9550-19-1-0177.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Ausiello, G., Crescenzi, P., Gambosi, G., Kann, V., Marchetti-Spaccamela, A., Protasi, M.: Complexity and Approximation: Combinatorial Optimization and Their Approximability Properties, 1st edn. Springer, Heidelberg (1999). https://doi.org/10.1007/978-3-642-58412-1
Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)
Cotton, S., Asarin, E., Maler, O., Niebert, P.: Some progress in satisfiability checking for difference logic. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 263–276. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_19
Cotton, S., Maler, O.: Fast and flexible difference constraint propagation for DPLL(T). In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 170–183. Springer, Heidelberg (2006). https://doi.org/10.1007/11814948_19
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252 (1977)
Cox, I.J., Rao, S.B., Zhong, Y.: Ratio regions: a technique for image segmentation. In: Proceedings of the International Conference on Pattern Recognition, pp. 557–564. IEEE, August 1996
Cygan, M., et al.: Parameterized Algorithms. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21275-3
Demtrescu, C., Italiano, G.F.: A new approach to dynamic all pairs shortest paths. J. ACM 51(6), 968–992 (2004)
Farkas, G.: Über die Theorie der Einfachen Ungleichungen. J. für die Reine und Angewandte Mathematik 124(124), 1–27 (1902)
Fleury, P.-H.: Deux problèmes de géométrie de situation. J. de mathématiques élémentaires, 2nd ser. 2, 257–261 (1883). (in French)
Gerber, R., Pugh, W., Saksena, M.: Parametric dispatching of hard real-time tasks. IEEE Trans. Comput. 44(3), 471–479 (1995)
Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39(2–3), 297–308 (1985)
Han, C.C., Lin, K.J.: Job scheduling with temporal distance constraints. Technical report UIUCDCS-R-89-1560, University of Illinois at Urbana-Champaign, Department of Computer Science (1989)
Iwama, K., Miyano, E.: Intractability of read-once resolution. In: Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC 1995), Los Alamitos, CA, USA, pp. 29–36. IEEE Computer Society Press, June 1995
Kann, V.: Polynomially bounded minimization problems that are hard to approximate. Nord. J. Comput. 1(3), 317–331 (1994)
Kleine Büning, H., Wojciechowski, P., Subramani, K.: Read-once resolutions in horn formulas. In: Chen, Y., Deng, X., Lu, M. (eds.) FAW 2019. LNCS, vol. 11458, pp. 100–110. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-18126-0_9
Nemhauser, G.L., Wolsey, L.A.: Integer and Combinatorial Optimization. Wiley, New York (1999)
Nieuwenhuis, R., Oliveras, A.: DPLL(T) with exhaustive theory propagation and its application to difference logic. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 321–334. Springer, Heidelberg (2005). https://doi.org/10.1007/11513988_33
John Alan Robinson: A machine-oriented logic based on the resolution principle. J. ACM 12(1), 23–41 (1965)
Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1987)
Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A hybrid sat-based decision procedure for separation logic with uninterpreted functions. In: DAC, pp. 425–430 (2003)
Subramani, K.: Optimal length resolution refutations of difference constraint systems. J. Autom. Reason. (JAR) 43(2), 121–137 (2009). https://doi.org/10.1007/s10817-009-9139-4
Subramani, K., Williamson, M., Gu, X.: Improved algorithms for optimal length resolution refutation in difference constraint systems. Formal Aspects Comput. 25(2), 319–341 (2013). https://doi.org/10.1007/s00165-011-0186-3
Subramani, K., Wojciechowki, P.: A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints. Algorithmica 81(7), 2765–2794 (2019). https://doi.org/10.1007/s00453-019-00554-z
Urquhart, A.: The complexity of propositional proofs. Bull. Symb. Log. 1(4), 425–467 (1995)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2021 Springer Nature Switzerland AG
About this paper
Cite this paper
Subramani, K., Wojciechowski, P. (2021). Analyzing Unit Read-Once Refutations in Difference Constraint Systems. In: Faber, W., Friedrich, G., Gebser, M., Morak, M. (eds) Logics in Artificial Intelligence. JELIA 2021. Lecture Notes in Computer Science(), vol 12678. Springer, Cham. https://doi.org/10.1007/978-3-030-75775-5_11
Download citation
DOI: https://doi.org/10.1007/978-3-030-75775-5_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-75774-8
Online ISBN: 978-3-030-75775-5
eBook Packages: Computer ScienceComputer Science (R0)