A Community-Division Based Algorithm for Finding Relations Among Linear Constraints
Abstract
Linear constraints are widely used in the modeling of many practical problems, and the solving technologies have important applications in satisfiability modulo theories, program analysis and verification. The efficiency of solving procedure could be improved by taking advantages of the relations among constraints. Traditional methods find relations through search, which do not take advantage of the structural characteristics and cost too much time. In this paper, a heuristic based on community division is proposed for finding relations among linear constraints. Firstly it builds a relation graph, which maps each constraint to a node. Then a division tool is employed to divide the nodes into several communities. At last, it tries to find relations among constraints in the same community through search. Experimental results show that the algorithm can effectively process large set of constraints, reduce time cost and find relations with higher quality.
Keywords
Linear constraint Relation finding Community division Constraint programmingNotes
Acknowledgement
This work is supported by National Natural Science Foundation of China (Grant No. 61672505), the National Key Basic Research (973) Program of China (Grant No. 2014CB340701), and Key Research Program of Frontier Sciences, CAS (Grant No. QYZDJ-SSW-JSC036). Feifei Ma is also supported by the Youth Innovation Promotion Association, CAS.
References
- 1.Blondel, V.D., Guillaume, J.L., Lambiotte, R., Lefebvre, E.: Fast unfolding of communities in large networks. J. Stat. Mech.: Theory Exp. 2008(10), P10008 (2008)CrossRefGoogle Scholar
- 2.Collavizza, H., Rueher, M., Van Hentenryck, P.: CPBPV: a constraint-programming framework for bounded program verification. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 327–341. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85958-1_22CrossRefGoogle Scholar
- 3.Dantzig, G.: Linear Programming and Extensions. Princeton University Press, Princeton (2016)Google Scholar
- 4.Estiningsih, Y., Farikhin, Tjahjana, R.: A comparison of heuristic method and Llewellyn’s rules for identification of redundant constraints. J. Phys. Conf. Ser. 983, 012083 (2018). IOP PublishingGoogle Scholar
- 5.Ge, C., Ma, F., Zhang, P., Zhang, J.: Computing and estimating the volume of the solution space of SMT (LA) constraints. Theor. Comput. Sci. (2016, in press)Google Scholar
- 6.Girvan, M., Newman, M.E.: Community structure in social and biological networks. Proc. Nat. Acad. Sci. 99(12), 7821–7826 (2002)MathSciNetCrossRefGoogle Scholar
- 7.Gotlieb, A.: TCAS software verification using constraint programming. Knowl. Eng. Rev. 27(3), 343–360 (2012)CrossRefGoogle Scholar
- 8.Huang, Z., Zhang, H., Zhang, J.: Improving first-order model searching by propositional reasoning and lemma learning. In: SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 10–13 May 2004, Vancouver, BC, Canada, Online Proceedings (2004)Google Scholar
- 9.de Moura, L.M., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)CrossRefGoogle Scholar
- 10.Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract davis-putnam-logemann-loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006)MathSciNetCrossRefGoogle Scholar
- 11.Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28(4), 765–768 (1981)MathSciNetCrossRefGoogle Scholar
- 12.Paulraj, S., Chellappan, C., Natesan, T.R.: A heuristic approach for identification of redundant constraints in linear programming models. Int. J. Comput. Math. 83(8&9), 675–683 (2006)MathSciNetCrossRefGoogle Scholar
- 13.Rardin, R.L.: Optimization in Operations Research. Prentice Hall, Upper Saddle River (2016)Google Scholar
- 14.Rossi, F., van Beek, P., Walsh, T. (eds.): Handbook of Constraint Programming, Foundations of Artificial Intelligence, vol. 2. Elsevier, New York City (2006)Google Scholar
- 15.Rybalchenko, A.: Constraint solving for program verification: theory and practice by example. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 57–71. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14295-6_7CrossRefGoogle Scholar
- 16.Silva, J.P.M., Sakallah, K.A.: Conflict analysis in search algorithms for satisfiability. In: Eigth International Conference on Tools with Artificial Intelligence, ICTAI 1996, Toulouse, France, 16–19 November 1996, pp. 467–469. IEEE Computer Society (1996)Google Scholar
- 17.Sumathi, P., Paulraj, S.: Identification of redundant constraints in large scale linear programming problems with minimal computational effort. Appl. Math. Sci. 7(80), 3963–3974 (2013)MathSciNetGoogle Scholar
- 18.Wang, J., Wang, X., Ma, Y., Wang, J.: Hierarchical combination design method of test cases based on conditional constraints. In: 2017 IEEE International Conference on Software Quality, Reliability and Security Companion, QRS-C 2017, Prague, Czech Republic, 25–29 July 2017, pp. 636–637. IEEE (2017)Google Scholar
- 19.Yan, J., Zhang, J., Xu, Z.: Finding relations among linear constraints. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS (LNAI), vol. 4120, pp. 226–240. Springer, Heidelberg (2006). https://doi.org/10.1007/11856290_20CrossRefGoogle Scholar
- 20.Yu, Y., Malik, S.: Lemma learning in SMT on linear constraints. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 142–155. Springer, Heidelberg (2006). https://doi.org/10.1007/11814948_17CrossRefGoogle Scholar
- 21.Zhang, J.: Specification analysis and test data generation by solving boolean combinations of numeric constraints. In: 1st Asia-Pacific Conference on Quality Software (APAQS 2000), 30–31 October 2000, Hong Kong, China, Proceedings, pp. 267–274. IEEE Computer Society (2000)Google Scholar
- 22.Zhang, J., Wang, X.: A constraint solver and its application to path feasibility analysis. Int. J. Softw. Eng. Knowl. Eng. 11(2), 139–156 (2001)CrossRefGoogle Scholar
- 23.Zhang, L., Malik, S.: The quest for efficient boolean satisfiability solvers. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 17–36. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45657-0_2CrossRefGoogle Scholar