17
$\begingroup$

In the past, I implemented coordination models using SAT and regular constraint satisfaction as the core workhorse in their engines. Continuing in this line of work, I would like to make the models more interactive, and the best way I see of doing this is to open up the constraint solver so that it is no longer a black box.

Thus, I'm interested in learning more about constraint satisfaction where the constraints have what I will call external variables, predicates and functions, that is, the constraint language may have predicates such as $\mathbf{P}(x)$ which can only be satisfied by consulting some agent external to the solver, and then only when $x$ is ground. A scenario where this is useful is whenever $\mathbf{P}$ corresponds to some external decision process that cannot be incorporated into the constraint solver. Such constraint solvers could be called open (as constraints are not entirely known) or interactive (as interaction is required to proceed with constraint satisfaction).

I would like to know both:

  • theoretical research done in this direction
  • tools or libraries that implement constraint solvers that allow interaction with the external world during the constraint solving process.
| cite | improve this question | |
$\endgroup$
9
$\begingroup$

I'm not altogether convinced by the previous work on open and interactive constraints.

An attempt to study the tractability questions was:

although this paper does leave several major questions unanswered. The approach via propagators in this paper is closely related to existing constraint solver implementations.

I think work on SMT (satisfiability modulo theories) is also closely related to your question. SMT theories are often motivated by problems from software and hardware verification, but there do exist theories with an AI flavour. I look forward to more applications built with SMT as the core technology, and to more work in constraints applying ideas from SMT.

| cite | improve this answer | |
$\endgroup$
  • 1
    $\begingroup$ That paper certainly looks interesting. I never thought of SMT solvers as doing what I require. It's certainly an avenue to explore. $\endgroup$ – Dave Clarke Oct 19 '10 at 12:44
  • $\begingroup$ I'm confused by the last comment. SMT solvers are for logics and theories, not specific predicates. People are welcome to contribute new theories and benchmarks. I know that the MathSAT developers have studied AI and planning problems. $\endgroup$ – Vijay D Sep 2 '11 at 2:52
  • $\begingroup$ @Vijay D: you are right, this sentence is unduly biased and I will revise it. An efficient implementation of INJECTIVE as an SMT theory was published in 2010 by Banković and Marić (argo.matf.bg.ac.rs/publications/2010/alldiff-smt2010.pdf). $\endgroup$ – András Salamon Sep 2 '11 at 14:18
7
$\begingroup$

Reading your question, I also agree in saying that Satisfiability Modulo Theories are closely related to your needs. I would suggest to read the book Decision Procedures - An Algorithmic Point of View.

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ How related/worthwhile is the book The Calculus of Computation: Decision Procedures with Applications to Verification by Aaron R. Bradley and Zohar Manna? I know where a copy of that is within walking distance. $\endgroup$ – Dave Clarke Oct 19 '10 at 13:29
  • $\begingroup$ @Dave: Disclaimer: My personal experience on SMT is just at the very beginning ;-) I've just looked at the Table of Contents of that book; there seems to be a big intersection between it and the one I've indicated. In the latter one, what you call here external functions is called there uninterpreted functions and is extensively covered. I was unable to find uninterpreted functions in the TOC of Decision Procedures with Applications to Verification; however, it seems to be a very good book and maybe it can turn out to be useful. $\endgroup$ – Giorgio Camerani Oct 19 '10 at 13:59
  • $\begingroup$ @Dave: In these days I'm reading Decision Procedures - An Algorithmic Point of View. I didn't yet reached the chapter about uninterpreted functions, but if I'm not wrong formulas with uninterpreted functions are converted to formulas in the Theory of Equality. It is the case that Theory of Equality is covered in Decision Procedures with Applications to Verification (Chapter 9). $\endgroup$ – Giorgio Camerani Oct 19 '10 at 14:09
  • 1
    $\begingroup$ I think Amazon is calling. $\endgroup$ – Dave Clarke Oct 19 '10 at 14:20
  • $\begingroup$ @Dave: OK, excellent! ;-) $\endgroup$ – Giorgio Camerani Oct 19 '10 at 14:35
7
$\begingroup$

For CSPs where you interact with the external world, there is also something called, unsurprisingly, Open CSP, defined in http://dx.doi.org/10.1016/j.artint.2004.10.005. The gist is that you don't know the satisfying/falsifying tuples of $\mathbf P(x)$, but discover them incrementally by querying a network. In my opinion, that paper does not do anything non-obvious, but it's a start.

| cite | improve this answer | |
$\endgroup$
4
$\begingroup$

I am a bit confused about the term interactive. I'll chime in with the others and add that an SMT solver might be helpful. To add to Walter Bishop's comment, slides for the Decision Procedures (Kroening and Strichman) book are available. John Harrison's thorough treatment in Handbook of Practical Logic and Automated Reasoning may also interest you. Example code is available online.

Philipp Ruemmer's Princess supports arithmetic with uninterpreted predicates, which might fit what you mean by open. It's written in Scala, uses E-matching in handling quantification and provides interpolants.

| cite | improve this answer | |
$\endgroup$
0
$\begingroup$

What about tools, if you decide to you Prolog as language of choice, I can suggest a few implementation approaches :

  • GNU Prolog with is C programming library. You can call C functions from Prolog, and Prolog from C. This opens you a lot of possibilities of extending functionality. Pro: Gnu Prolog is one of fastest freely available Prolog compilers. Note: Some people complain on lack of some build-in predicates... actually most of them can be implemented, check out Prolog compatibility layers @SO
  • SWI-Prolog has interesting programming library, including network communication, Protocol Buffers Support etc. And is quite popular.
  • XSB Prolog some people claim it's most interesting project in terms of interoperability - including : databases interfaces etc.

Prolog is programming language, that is suitable for doing many kinds of solvers (and most of them have their finite domain solvers).

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.