Advertisement

Constraints

, Volume 20, Issue 4, pp 414–432 | Cite as

On getting rid of the preprocessing minimization step in MUC-finding algorithms

  • Éric Grégoire
  • Jean-Marie Lagniez
  • Bertrand Mazure
Article

Abstract

When a constraint network is unsatisfiable, it can be of prime importance to provide the network designer with a full-fledged explanation of what causes the absence of any solution to the network. In this respect, minimal unsatisfiable cores (in short, MUCs) form the basis for such an explanation. Efficient MUC extractors are often made of an initial incomplete minimization step that delivers an upper-approximation of a MUC, followed by a refinement step. The first step is believed crucial for the global performance of the whole approach. In this paper, its actual importance is investigated. Especially, it is shown that the first step can be skipped when the refinement process dynamically exploits the information from its own search.

Keywords

CSP Constraint networks MUC Unsatisfiability 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bakker, R.R., Dikker, F., Tempelman, F., & Wognum, P.M. (1993). Diagnosing and solving over-determined constraint satisfaction problems. In Proceedings of the 13th International Joint Conference on Artificial Intelligence (IJCAI’93), vol. 1, pp. 276–281.Google Scholar
  2. 2.
    Belov, A., Järvisalo, M., & Marques-Silva, J. (2013). Formula preprocessing in MUS extraction. In N. Piterman, & S. Smolka (Eds.) Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2013), Lecture Notes in Computer Science, vol. 7795, pp. 110–125. Springer.Google Scholar
  3. 3.
    Belov, A., Lynce, I., & Marques-Silva, J. (2012). Towards efficient MUS extraction. AI Commununications, 97–116.Google Scholar
  4. 4.
    Belov, A., & Marques-Silva, J. (2011). Accelerating MUS extraction with recursive model rotation. In Proceedings of the 11th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2011), pp. 37–40. FMCAD.Google Scholar
  5. 5.
    Belov, A., & Marques-Silva, J. (2012). MUSer2: An efficient MUS extractor, system description. Journal on Satisfiability. Boolean Modeling and Computation, 8, 123–128.Google Scholar
  6. 6.
    Boussemart, F., Hémery, F., & Lecoutre, C. (2004). Saïs, L.: Boosting systematic search by weighting constraints. In Proceedings of the 16th European Conference on Artificial Intelligence (ECAI’04), pp. 482–486. Valencia (Spain).Google Scholar
  7. 7.
    (2008). Third international CSP solver competition http://cpai.ucc.ie/08/.
  8. 8.
    (2009). Fourth international constraint solver competition http://cpai.ucc.ie/09/.
  9. 9.
    Eiter, T., & Gottlob, G. (1992). On the complexity of propositional knowledge base revision, updates and counterfactual. Artificial Intelligence, 57, 227–270.MathSciNetCrossRefMATHGoogle Scholar
  10. 10.
    Grégoire, É., Lagniez, J.M., & Mazure, B. (2011). A CSP solver focusing on FAC variables. In Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming (CP’11), Lecture Notes in Computer Science, vol. 6876, pp. 493–507. Springer.Google Scholar
  11. 11.
    Grégoire, É., Lagniez, J. M., & Mazure, B. (2012). Relax!. In Proceedings of the 24th IEEE International Conference on Tools with Artificial Intelligence (ICTAI’12), pp. 146–153. IEEE Computer Press.Google Scholar
  12. 12.
    Grégoire, É., Lagniez, J.M., & Mazure, B. (2013). Preserving partial solutions while relaxing constraint networks. In Proceedings of the 23th International Joint Conference on Artificial Intelligence (IJCAI’13) (pp. 552–558). China: Beijing.Google Scholar
  13. 13.
    Grégoire, É., Lagniez, J.M., & Mazure, B. (2014). Boosting MUC extraction in unsatisfiable constraint networks. Applied Intelligence, 1–12.Google Scholar
  14. 14.
    Grégoire, E., Mazure, B., & Piette, C. (2006). Extracting MUSes. In Proceedings of the 17th European Conference on Artificial Intelligence (ECAI’06), pp. 387–391.Google Scholar
  15. 15.
    Grėgoire, Ė., Mazure, B., & Piette, C. (2006). Tracking MUSes and strict inconsistent covers. In Proceedings of the 6th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2006), pp. 39–46.Google Scholar
  16. 16.
    Grėgoire, Ė., Mazure, B., & Piette, C. (2007). MUST: provide a finer-grained explanation of unsatisfiability. In Proceedings of 13th International Conference on Principles and Practice of Constraint Programming (CP’07), pp. 317–331.Google Scholar
  17. 17.
    Grégoire, É., Mazure, B., & Piette, C. (2008). On finding minimally unsatisfiable cores of CSPs. International Journal on Artificial Intelligence Tools (IJAIT), 17(4), 745–763.CrossRefGoogle Scholar
  18. 18.
    Grégoire, É., Mazure, B., & Piette, C. (2006). Saïs, L.: A new heuristic-based albeit complete method to extract MUCs from unsatisfiable CSPs. In Proceedings of the IEEE International Conference on Information Reuse and Integration (IEEE-IRI’06), pp. 325–329.Google Scholar
  19. 19.
    Hémery, F., Lecoutre, C., Saïs, L., & Boussemart, F. (2006). Extracting MUCs from constraint networks. In Proceedings of the 17th European Conference on Artificial Intelligence (ECAI’06), pp. 113–117.Google Scholar
  20. 20.
    Junker, U. (2001). QuickXplain: Conflict detection for arbitrary constraint propagation algorithms, IJCAI’01 Workshop on Modelling and Solving Problems with Constraints (CONS-1).Google Scholar
  21. 21.
    Junker, U. (2004). QuickXplain: Preferred explanations and relaxations for over-constrained problems. In Proceedings of the 19th National Conference on Artificial Intelligence (AAAI’04), pp. 167–172.Google Scholar
  22. 22.
    Jussien, N., & Barichard, V. (2000). The PaLM system: explanation-based constraint programming. In Proceedings of TRICS: Techniques foR Implementing Constraint programming Systems, Post-conference workshop of CP’00, pp. 118–133.Google Scholar
  23. 23.
    Laburthe, F., & OCRE Project Team, T. Choco: implementing a CP kernel. In Proceedings of TRICS: Techniques foR Implementing Constraint programming Systems, Post-conference Workshop of CP’00. Singapore (2000). http://www.choco-constraints.net.
  24. 24.
    Lagniez, J.M., & Biere, A. (2013). Factoring out assumptions to speed up MUS extraction. In Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT’11), Lecture Notes in Computer Science, vol. 6695, pp. 276–292. Springer.Google Scholar
  25. 25.
    Lagniez, J.M., Grégoire, É., & Mazure, B. (2012). A data structure boosting the performance of local search for CSP solving. In International Conference on heuristics and Nature Inspired Computing (META’12). Paper also available from the authors’ webpages http://www.cril.univ-artois.fr/lagniez/publication.html.
  26. 26.
    Lecoutre, C. (2009). Constraint Networks: Techniques and Algorithms. Wiley: International Scientific and Technical Encyclopedia.CrossRefGoogle Scholar
  27. 27.
    Mackworth, A.K. (1977). Consistency in networks of relations. Artificial Intelligence, 8(1), 99–118.MathSciNetCrossRefMATHGoogle Scholar
  28. 28.
    McAllester, D., Selman, B., & Kautz, H.A. (1997). Evidence for invariants in local search. In Fourteenth National Conference on Artificial Intelligence (AAAI’97), pp. 321–326.Google Scholar
  29. 29.
    Nadel, A. (2010). Boosting minimal unsatisfiable core extraction. In Proceedings of the 10th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2010), pp. 221–229. IEEE.Google Scholar
  30. 30.
    (2014). In O’Sullivan, B. (Ed.) Proceedings of the 19th International Conference on Principles and Practice of Constraint Programming (CP’2014), Lecture Notes in Computer Science, vol. 8656: Springer.Google Scholar
  31. 31.
    Papadimitriou, C.H., & Wolfe, D. (1988). The complexity of facets resolved. Journal of Computer and System Sciences, 37(1), 2–13.MathSciNetCrossRefMATHGoogle Scholar
  32. 32.
    Pesant, G. (ed.) (2014). Constraints (Journal), vol. 19, Springer.Google Scholar
  33. 33.
    Rossi, F., van Beek, P., & Walsh, T. (eds.) (2006). Handbook of constraint programming. Elsevier Science.Google Scholar
  34. 34.
    Ryvchin, V., & Strichman, O. (2011). Faster extraction of high-level minimal unsatisfiable cores. In Proceedings of the 14th International Conference on Theory and Applications of Satisfiability Testing, Lecture Notes in Computer Science, vol. 6695, pp. 174–187.Google Scholar
  35. 35.
    (2014). In Simonis, H. (Ed.) Proceedings of the 11th International Conference on Integration of AI and OR Techniques in Constraint Programming (CPAIOR’2014), Lecture Notes in Computer Science, vol. 8451: Springer.Google Scholar
  36. 36.
    de Siqueira, N., J., & Puget, J.F. (1988). Explanation-based generalization of failures. In Proceedings of the Eighth European Conference on Artificial Intelligence (ECAI’88), pp. 339–344.Google Scholar
  37. 37.
    Wieringa, S. (2012). Understanding, improving and parallelizing MUS finding using model rotation. In Proceedings of the 18th International Conference on Principles and Practice of Constraint Programming (CP’12), Lecture Notes in Computer Science, vol. 7514, pp. 672–687. Springer.Google Scholar

Copyright information

© Springer Science+Business Media New York 2015

Authors and Affiliations

  • Éric Grégoire
    • 1
  • Jean-Marie Lagniez
    • 1
  • Bertrand Mazure
    • 1
  1. 1.CRIL, CNRS umr 8188Université d’Artois rue Jean Souvraz SP18LensFrance

Personalised recommendations