×

Implementing logical connectives in constraint programming. (English) Zbl 1210.68103

Summary: Combining constraints using logical connectives such as disjunction is ubiquitous in constraint programming, because it adds considerable expressive power to a constraint language. We explore the solver architecture needed to propagate such combinations of constraints efficiently. In particular we describe two new features named satisfying sets and constraint trees. We also make use of movable triggers [I. P. Gent, C. Jefferson and I. Miguel, “Watched literals for constraint propagation in minion”, Lect. Notes Comput. Sci. 4204, 182–197 (2006)], and with these three complementary features we are able to make considerable efficiency gains.
A key reason for the success of Boolean Satisfiability (SAT) solvers is their ability to propagate Or constraints efficiently, making use of movable triggers. We successfully generalise this approach to an Or of an arbitrary set of constraints, maintaining the crucial property that at most two constraints are active at any time, and no computation at all is done on the others. We also give an And propagator within our framework, which may be embedded within the Or. Using this approach, we demonstrate speedups of over 10,000 times in some cases, compared to traditional constraint programming approaches. We also prove that the Or algorithm enforces generalised arc consistency (GAC) when all its child constraints have a GAC propagator, and no variables are shared between children. By extending the Or propagator, we present a propagator for AtLeastK, which expresses that at least \(k\) of its child constraints are satisfied in any solution.
Some logical expressions (e.g. exclusive-or) cannot be compactly expressed using And, Or and AtLeastK. Therefore we investigate reification of constraints. We present a fast generic algorithm for reification using satisfying sets and movable triggers.

MSC:

68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

Software:

Chaff; MINION
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Gent, I. P.; Jefferson, C.; Miguel, I., Watched literals for constraint propagation in minion, (Benhamou, F., CP. CP, Lecture Notes in Computer Science, vol. 4204 (2006), Springer), 182-197 · Zbl 1420.68195
[2] Apt, K. R., Principles of Constraint Programming (2003), Cambridge University Press · Zbl 1187.68132
[3] (Rossi, F.; van Beek, P.; Walsh, T., Handbook of Constraint Programming (2006), Elsevier)
[4] Gent, I. P.; Jefferson, C.; Miguel, I., Minion: A fast scalable constraint solver, (Brewka, G.; Coradeschi, S.; Perini, A.; Traverso, P., ECAI. ECAI, Frontiers in Artificial Intelligence and Applications, vol. 141 (2006), IOS Press), 98-102
[5] Brand, S.; Yap, R. H.C., Towards “propagation = logic + control”, (Etalle, S.; Truszczynski, M., ICLP. ICLP, Lecture Notes in Computer Science, vol. 4079 (2006), Springer), 102-116 · Zbl 1131.68368
[6] Müller, T.; Würtz, J., Constructive disjunction in Oz, (Workshop Logische Programmierung (WLP). Workshop Logische Programmierung (WLP), GMD-Studien, vol. 270 (1995), Gesellschaft für Mathematik und Datenverarbeitung MBH), 113-122
[7] Würtz, J.; Müller, T., Constructive disjunction revisited, (Görz, G.; Hölldobler, S., German Conference on Artificial Intelligence (KI). German Conference on Artificial Intelligence (KI), LNCS, vol. 1137 (1996), Springer), 377-386
[8] Lagerkvist, M. Z.; Schulte, C., Propagator groups, (Gent, I. P., CP. CP, Lecture Notes in Computer Science, vol. 5732 (2009), Springer), 524-538
[9] Bacchus, F.; Walsh, T., Propagating logical combinations of constraints, (Kaelbling, L. P.; Saffiotti, A., IJCAI (2005), Professional Book Center), 35-40
[10] Lhomme, O., An efficient filtering algorithm for disjunction of constraints, (Rossi, F., CP. CP, Lecture Notes in Computer Science, vol. 2833 (2003), Springer), 904-908
[11] Lhomme, O., Arc-consistency filtering algorithms for logical combinations of constraints, (Régin, J. C.; Rueher, M., CPAIOR. CPAIOR, Lecture Notes in Computer Science, vol. 3011 (2004), Springer), 209-224 · Zbl 1094.68648
[12] Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S., Chaff: engineering an efficient sat solver, (DAC ’01: Proceedings of the 38th Annual Design Automation Conference (2001), ACM: ACM New York, NY, USA), 530-535
[15] Aggoun, A.; Chan, D.; Dufresne, P.; Falvey, E.; Grant, H.; Harvey, W.; Herold, A.; Macartney, G.; Meier, M.; Miller, D.; Mudambi, S.; Novello, S.; Perez, B.; van Rossum, E.; Schimpf, J.; Shen, K.; Tsahageas, P. A.; de Villeneuve, D. H., Eclipse user manual release 5.10 (2006)
[16] Schulte, C., Programming deep concurrent constraint combinators, (Proceedings of Practical Aspects of Declarative Languages (PADL 2000). Proceedings of Practical Aspects of Declarative Languages (PADL 2000), LNCS, vol. 1753 (2000), Springer), 215-229
[17] Bessiere, C.; Hebrard, E.; Hnich, B.; Walsh, T., The complexity of reasoning with global constraints, Constraints, 12, 2, 239-259 (2007) · Zbl 1124.68103
[19] Colbourn, C. J.; Dinitz, J. H., Handbook of Combinatorial Designs, Discrete Mathematics and Its Applications (2006), Chapman & Hall/CRC
[20] Daniel, P.; Semple, C., Supertree algorithms for nested taxa, (Bininda-Emonds, O., Phylogenetic Supertrees: Combining Information to Reveal the Tree of Life. Phylogenetic Supertrees: Combining Information to Reveal the Tree of Life, Computational Biology Series (2004), Kluwer), 151-171
[21] Gent, I. P.; Prosser, P.; Smith, B. M.; Wei, W., Supertree construction with constraint programming, (Rossi, F., CP. CP, Lecture Notes in Computer Science, vol. 2833 (2003), Springer), 837-841
[22] Moore, N. C.; Prosser, P., The ultrametric constraint and its application to phylogenetics, Journal of Artificial Intelligence Research, 32, 901-938 (2008) · Zbl 1166.92033
[24] Gent, I. P.; Jefferson, C.; Kelsey, T.; Lynce, I.; Miguel, I.; Nightingale, P.; Smith, B. M., Search in the patience game ‘black hole’, AI Communications, 20, 3, 211-226 (2007) · Zbl 1151.90525
[25] Gent, I. P.; Miguel, I.; Nightingale, P., Generalised arc consistency for the alldifferent constraint: An empirical survey, Artificial Intelligence, 172, 18, 1973-2000 (2008) · Zbl 1184.68472
[26] Jefferson, C.; Miguel, A.; Miguel, I.; Tarim, A., Modelling and solving English peg solitaire, Computers and Operations Research, 33, 10, 2935-2959 (2006) · Zbl 1086.90070
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.