×

The logic of constraint satisfaction. (English) Zbl 0782.68104

Summary: The constraint satisfaction problem (CSP) formalization has been a productive tool within Artificial Intelligence and related areas. The finite CSP (FCSP) framework is presented here as a restricted logical calculus within a space of logical representation and reasoning systems. FCSP is formulated in a variety of logical settings: theorem proving in first order predicate calculus, propositional theorem proving (and hence SAT), the Prolog and Datalog approaches, constraint network algorithms, a logical interpreter for networks of constraints, the constraint logic programming (CLP) paradigm and propositional model finding (and hence SAT, again). Several standard, and some not-so-standard, logical methods can therefore be used to solve these problems. By doing this we obtain a specification of the semantics of the common approaches. This synthetic treatment also allows algorithms and results from these disparate areas to be imported, and specialized, to FCSP; the special properties of FCSP are exploited to achieve, for example, completeness and to improve efficiency. It also allows export to the related areas. By casting CSP both as a generalization of FCSP and as a specialization of CLP it is observed that some, but not all, FCSP techniques lift to CSP and thereby to CLP. Various new connections are uncovered, in particular between the proof-finding approaches and the alternative model-finding approaches that have arisen in depiction and diagnosis applications.

MSC:

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)

Keywords:

finite CSP
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bibel, W., Constraint satisfaction from a deductive viewpoint, Artif. Intell., 35, 401-413 (1988) · Zbl 0645.68112
[2] Clark, K. L., Negation as failure, (Gallaire, H.; Minker, J., Logic and Databases (1978), Plenum Press: Plenum Press New York), 293-322
[3] Davis, E., Constraint propagation with interval labels, Artif. Intell., 32, 281-331 (1987) · Zbl 0642.68176
[4] de Kleer, J., A comparison of ATMS and CSP techniques, (Proceedings IJCAI-89. Proceedings IJCAI-89, Detroit, MI (1989)), 290-296 · Zbl 0707.68096
[5] de Kleer, J.; Mackworth, A. K.; Reiter, R., Characterizing diagnoses, (Proceedings AAAI-90. Proceedings AAAI-90, Boston, MA (1990)), 324-330
[6] Dechter, R., Constraint networks, (Shapiro, S. C., The Encyclopedia of AI (1992), Wiley: Wiley New York), 276-285
[7] Dechter, R.; Pearl, J., Directed constraint networks, (Proceedings IJCAI-91. Proceedings IJCAI-91, Sydney, Australia (1991)), 1164-1170 · Zbl 0761.68087
[8] Dowling, W. F.; Gallier, J. H., Linear-time algorithms for testing the satisfiability of propositional Horn formulae, J. Logic Program, 3, 267-284 (1984) · Zbl 0593.68062
[9] Enderton, H. B., (A Mathematical Introduction to Logic (1972), Academic Press: Academic Press Orlando, FL)
[10] Even, S.; Itai, A.; Shamir, A., On the complexity of timetable and multicommodity flow problems, SIAM J. Comput., 5, 4, 691-703 (1976) · Zbl 0358.90021
[11] Freuder, E. C., Complexity of \(k\)-tree structured constraint satisfaction problems, (Proceedings AAAI-90. Proceedings AAAI-90, Boston, MA (1990)), 4-9
[12] Jaffar, J.; Lassez, J.-L., Constraint logic programming, (Proceedings 14th ACM Principles of Programming Languages Conference. Proceedings 14th ACM Principles of Programming Languages Conference, Munich, Germany (1987)), 111-119
[13] Jones, N. D.; Lien, Y. E.; Laaser, W. T., New problems complete for nondeterministic log space, Math. Syst. Theor., 10, 1-17 (1976) · Zbl 0341.68035
[14] Kasif, S., Parallel solutions to constraint satisfaction problems, (Proceedings First International Conference on Principles of Knowledge Representation and Reasoning. Proceedings First International Conference on Principles of Knowledge Representation and Reasoning, Toronto, Ont. (1989)), 180-188
[15] Kowalski, R., A proof procedure using connection graphs, J. ACM, 22, 4, 572-595 (1975) · Zbl 0357.68097
[16] Mackworth, A. K., Consistency in networks of relations, Artif. Intell., 8, 99-118 (1977) · Zbl 0341.68061
[17] Mackworth, A. K., Constraint satisfaction, (Shapiro, S. C., The Encyclopedia of AI (1992), Wiley: Wiley New York), 285-293
[18] Mackworth, A. K.; Freuder, E. C., The complexity of some polynomial network consistency algorithms for constraint satisfaction problems, Artif. Intell., 25, 65-74 (1985)
[19] Maier, D., (The Theory of Relational Databases (1983), Computer Science Press: Computer Science Press Rockville, MD) · Zbl 0519.68082
[20] McAllester, D. A., Truth maintenance, (Proceedings AAAI-90. Proceedings AAAI-90, Boston, MA (1990)), 1109-1116
[21] Montanari, U., Networks of constraints: fundamental properties and applications to picture processing, Inf. Sci., 7, 95-132 (1974) · Zbl 0284.68074
[22] Montanari, U.; Rossi, F., Constraint relaxation may be perfect, Artif. Intell., 48, 2, 143-170 (1991) · Zbl 1117.68495
[23] Reiter, R., Nonmonotonic reasoning, (Shrobe, H. E., Exploring Artificial Intelligence (1988), Morgan Kaufmann: Morgan Kaufmann San Mateo, CA), 439-482
[24] Reiter, R.; Mackworth, A. K., A logical framework for depiction and image interpretation, Artif. Intell., 41, 125-155 (1989) · Zbl 0689.68113
[25] Seidel, R., A new method for solving constraint satisfaction problems, (Proceedings IJCAI-81. Proceedings IJCAI-81, Vancouver, BC (1981)), 338-342
[26] Sidebottom, G.; Havens, W. S., Hierarchical arc consistency applied to numeric processing in constraint logic programming, (Tech. Rept. CSS-IS TR 91-06 (1991), Simon Fraser University: Simon Fraser University Burnaby, BC)
[27] Van Hentenryck, P., (Constraint Satisfaction in Logic Programming (1989), MIT Press: MIT Press Cambridge, MA)
[28] Zhang, Y.; Mackworth, A. K., Parallel and distributed algorithms for constraint satisfaction problems, (Proceedings 3rd IEEE Symposium on Parallel and Distributed Processing. Proceedings 3rd IEEE Symposium on Parallel and Distributed Processing, Dallas, TX (1991)), 394-397
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.