Abstract
We introduce WSimply, a new framework for modelling and solving Weighted Constraint Satisfaction Problems (WCSP) using Satisfiability Modulo Theories (SMT) technology. In contrast to other well-known approaches designed for extensional representation of goods or no-goods, and with few declarative facilities, our approach aims to follow an intensional and declarative syntax style. In addition, our language has built-in support for some meta-constraints, such as priority and homogeneity, which allows the user to easily specify rich requirements on the desired solutions, such as preferences and fairness. We propose two alternative strategies for solving these WCSP instances using SMT. The first is the reformulation into Weighted SMT (WSMT) and the application of satisfiability test based algorithms from recent contributions in the Weighted Maximum Satisfiability field. The second one is the reformulation into an operation research-like style which involves an optimisation variable or objective function and the application of optimisation SMT solvers. We present experimental results of two well-known problems: the Nurse Rostering Problem (NRP) and a variant of the Balanced Academic Curriculum Problem (BACP), and provide some insights into the impact of the addition of meta-constraints on the quality of the solutions and the solving time.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Ansótegui, C., Bofill, M., Palahí, M., Suy, J., Villaret, M. (2011). A proposal for solving Weighted CSPs with SMT. In Proceedings of the 10th international workshop on constraint modelling and reformulation (ModRef 2011) (pp. 5–19).
Ansótegui, C., Bofill, M., Palahí, M., Suy, J., Villaret, M. (2011). Satisfiability modulo theories: An efficient approach for the resource-constrained project scheduling problem. In Proceedings of the 9th symposium on abstraction, reformulation and approximation (SARA 2011) (pp. 2–9).
Ansótegui, C., Bofill, M., Palahí, M., Suy, J., Villaret, M. (2011). W-MiniZinc: A proposal for modeling weighted CSP with MiniZinc. In Proceedings of the 1st international workshop on MiniZinc (MZN 2011).
Ansótegui, C., Bonet, M.L., Levy, J. (2009). Solving (weighted) partial MaxSAT through satisfiability testing. In Proceedings of the twelfth international conference on theory and applications of satisfiability testing (SAT 2009). LNCS (Vol. 5584, pp. 427–440). Springer.
Barrett, C., Stump, A., Tinelli, C. (2010). The SMT-LIB standard: Version 2.0. In A. Gupta, & D. Kroening (Eds.), Proceedings of the 8th international workshop on satisfiability modulo theories. UK: Edinburgh.
Biere, A. (2008). Picosat essentials. Journal on Satisfiability, Boolean Modeling and Computation, 4(2–4), 75–97.
Bofill, M., Palahí, M., Suy, J., Villaret, M. (2009). SIMPLY: A compiler from a CSP modeling language to the SMT-LIB format. In Proceedings of the eighth international workshop on constraint Modelling and Reformulation (ModRef 2009) (pp. 30–44).
Bofill, M., Palahí, M., Suy, J., Villaret, M. (2012). Solving constraint satisfaction problems with SAT modulo theories. Constraints, 17(3), 273–303.
Burke, E.K., Causmaecker, P.D., Berghe, G.V., Landeghem, H.V. (2004). The state of the art of nurse rostering. Journal of Scheduling, 7(6), 441–499.
Castro, C., & Manzano, S. (2001). Variable and value ordering when solving balanced academic curriculum problems. In 6th annual workshop of the ERCIM working group on constraints.
Cooper, M.C., DeGivry, S., Schiex, T. (2007). Optimal soft arc consistency. In Proceedings of the 20th international joint conference on artificial intelligence (IJCAI 2007) (pp. 68–73).
deGivry, S., Zytnicki, M., Heras, F., Larrosa, J. (2005). Existential arc consistency: Getting closer to full arc consistency in weighted CSPs. In Proceedings of the 19th international joint conference on artificial intelligence (IJCAI 2005) (pp. 84–89).
Dutertre, B., & deMoura, L. (2006). A fast linear-arithmetic solver for DPLL(T). In Proceedings of the 18th international conference on computer aided verification, CAV’06. LNCS (Vol. 4144, pp. 81–94). Springer.
Dutertre, B., & deMoura, L. (2006). The Yices SMT solver. Tool paper available at http://yices.csl.sri.com/tool-paper.pdf.
Eén, N., & Sörensson, N. (2003). An extensible sat-solver. In E. Giunchiglia, & A. Tacchella (Eds.), SAT. Lecture notes in computer science (Vol. 2919, pp. 502–518). Springer.
Freuder, E.C., & Wallace, R.J. (1992). Partial constraint satisfaction. Artificial Intelligence, 58(1–3), 21–70.
Frisch, A.M., Harvey, W., Jefferson, C., Martínez-Hernández, B., Miguel, I. (2008). Essence: a constraint language for specifying combinatorial problems. Constraints, 13(3), 268–306.
Gent, I., Miguel, I., Rendl, A. (2010). Optimising quantified expressions in constraint models. In Proceedings of the 9th international workshop on constraint modelling and reformulation (ModRef 2010).
Hnich, B., Kiziltan, Z., Walsh, T. (2002). Modelling a balanced academic curriculum problem. In Proceedings of the fourth international workshop on integration of AI and OR techniques in constraint programming for combinatorial optimisation problems (CPAIOR 2002) (pp. 121–131).
Larrosa, J., & Meseguer, P. (2002). Partition-based lower bound for max-CSP. Constraints, 7, 407–419.
Larrosa, J., Meseguer, P., Schiex, T. (1999). Maintaining reversible DAC for max-CSP. Artificial Intelligence, 107(1), 149–163.
Larrosa, J., & Schiex, T. (2004). Solving weighted CSP by maintaining arc-consistency. Artificial Intelligence, 159(1–2), 1–26.
Mahajan, Y.S., Fu, Z., Malik, S. (2004). Zchaff2004: An efficient SAT solver. In H.H. Hoos, & D.G. Mitchell (Eds.), Proceedings of the 7th international conference on theory and applications of satisfiability testing (SAT 2004). LNCS (Vol. 3542, pp. 360–375). Springer.
Manquinho, V.M., Silva, J.P.M., Planes, J. (2009). Algorithms for weighted Boolean optimization. In Proceedings of the twelfth international conference on theory and applications of satisfiability testing (SAT 2009). LNCS (Vol. 5584, pp. 495–508). Springer.
Meseguer, P., Rossi, F., Schiex, T. (2006). Soft constraints. In F. Rossi, P. van Beek, T. Walsh (Eds.), Handbook of constraint programming (chapter 9). Elsevier.
Métivier, J.-P., Boizumault, P., Loudni, S. (2009). Solving nurse rostering problems using soft global constraints. In Proceedings of the 15th international conference on principles and practice of constraint programming (CP 2009). LNCS (Vol. 5732, pp. 73–87). Springer.
Michel, L., See, A., VanHentenryck, P. (2009). Parallel and distributed local search in COMET. Computers and Operations Research, 36, 2357–2375.
Nethercote, N., Stuckey, P.J., Becket, R., Brand, S., Duck, G.J., Tack, G. (2007). MiniZinc: Towards a standard CP modelling language. In Proceedings of the 13th international conference on principles and practice of constraint programming (CP 2007). LNCS (Vol. 4741, pp. 529–543). Springer.
Nieuwenhuis, R., & Oliveras, A. (2006). On SAT modulo theories and optimization problems. In Proceedings of the 9th international conference on theory and applications of satisfiability testing (SAT 2006). LNCS (Vol. 4121, pp. 156–169). Springer.
Nieuwenhuis, R., Oliveras, A., Tinelli, C. (2006). Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). Journal of the ACM, 53(6), 937–977.
Palahí, M. (2010). Eines basades en la lògica per a modelatges i resolució de problemes combinatoris. Master’s thesis, Universitat de Girona/Universitat Politècnica de Catalunya, Spain.
Petit, T., Regin, J.C., Bessiere, C. (2000). Meta-constraints on violations for over constrained problems. In 12th IEEE international conference on tools with artificial intelligence (ICTAI 2000) (pp. 358–365).
Roussel, O., & Lecoutre, C. (2009). XML representation of constraint networks: format XCSP 2.1. Computing Research Repository, abs/0902.2362. http://arxiv.org/abs/0902.2362.
Sebastiani, R. (2007). Lazy satisability modulo theories. Journal on Satisfiability, Boolean Modeling and Computation, 3(3–4), 141–224.
Vanhoucke, M., & Maenhout, B. (2007). NSPLib—a nurse scheduling problem library: A tool to evaluate (meta-) heuristic procedures. In Operational research for health policy making better decisions (pp. 151–165).
Author information
Authors and Affiliations
Corresponding author
Additional information
This work is an extended version of the paper [1] presented at the ModRef 2011 workshop. Research partially supported by the Generalitat de Catalunya under grant AGAUR 2009-SGR-1434, and the Ministerio de Economía y Competividad research projects TIN2008-04547, TIN2009-14704-C03-01, and TIN2010-20967-C04-01/03.
Rights and permissions
About this article
Cite this article
Ansótegui, C., Bofill, M., Palahí, M. et al. Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories. Constraints 18, 236–268 (2013). https://doi.org/10.1007/s10601-012-9131-1
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10601-012-9131-1