Advertisement

A Community-Division Based Algorithm for Finding Relations Among Linear Constraints

  • Minghao Liu
  • Feifei Ma
  • Jun Yan
Conference paper
First Online:
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11062)

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 programming 
This is a preview of subscription content, log in to check access.

Notes

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. 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. 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. 3.
    Dantzig, G.: Linear Programming and Extensions. Princeton University Press, Princeton (2016)Google Scholar
  4. 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. 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. 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. 7.
    Gotlieb, A.: TCAS software verification using constraint programming. Knowl. Eng. Rev. 27(3), 343–360 (2012)CrossRefGoogle Scholar
  8. 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. 9.
    de Moura, L.M., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)CrossRefGoogle Scholar
  10. 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. 11.
    Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28(4), 765–768 (1981)MathSciNetCrossRefGoogle Scholar
  12. 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. 13.
    Rardin, R.L.: Optimization in Operations Research. Prentice Hall, Upper Saddle River (2016)Google Scholar
  14. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.State Key Laboratory of Computer Science, Institute of SoftwareChinese Academy of SciencesBeijingChina
  2. 2.Laboratory of Parallel Software and Computational Science, Institute of SoftwareChinese Academy of SciencesBeijingChina
  3. 3.Technology Center of Software Engineering, Institute of SoftwareChinese Academy of SciencesBeijingChina
  4. 4.University of Chinese Academy of SciencesBeijingChina

Personalised recommendations

Cite paper

Buy options