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

<p>An attempt to study the tractability questions was:</p>

<ul>
<li>Martin J. Green and Christopher Jefferson, <em>Structural Tractability of Propagated Constraints</em>, CP 2008.
doi: <a href="http://dx.doi.org/10.1007/978-3-540-85958-1_25" rel="nofollow">10.1007/978-3-540-85958-1_25</a></li>
</ul>

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

<p>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.</p>

CC BY-SA 3.0
2011-09-02T02:52:25.597Z
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.
Vijay D
CC BY-SA 3.0
2011-09-02T14:18:05.220Z
@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ć (http://argo.matf.bg.ac.rs/publications/2010/alldiff-smt2010.pdf).
András Salamon
CC BY-SA 2.5
2010-10-19T12:44:03.213Z
That paper certainly looks interesting. I never thought of SMT solvers as doing what I require. It's certainly an avenue to explore.
Dave Clarke
CC BY-SA 3.0
2010-10-19T12:01:15.750Z
2011-09-02T14:35:44.037Z
2011-09-02T14:35:44.037Z
András Salamon
<p>For CSPs where you interact with the external world, there is also something called, unsurprisingly, Open CSP, defined in <a href="http://dx.doi.org/10.1016/j.artint.2004.10.005">http://dx.doi.org/10.1016/j.artint.2004.10.005</a>. 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.</p>

CC BY-SA 2.5
2010-10-21T16:58:39.050Z
2010-10-21T16:58:39.050Z
Evgenij Thorstensen
<p>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 <a href="http://www.decision-procedures.org">Decision Procedures - An Algorithmic Point of View</a>.</p>

CC BY-SA 2.5
2010-10-19T13:29:22.480Z
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.
Dave Clarke
CC BY-SA 2.5
2010-10-19T13:59:39.073Z
@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.
Giorgio Camerani
CC BY-SA 2.5
2010-10-19T14:09:35.767Z
@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).
Giorgio Camerani
CC BY-SA 2.5
2010-10-19T14:20:39.640Z
I think Amazon is calling.
Dave Clarke
CC BY-SA 2.5
2010-10-19T14:35:41.387Z
@Dave: OK, excellent! ;-)
Giorgio Camerani
CC BY-SA 2.5
2010-10-19T13:22:16.797Z
2010-10-19T13:22:16.797Z
Giorgio Camerani
<p>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, <a href="http://www.decision-procedures.org/slides/" rel="nofollow">slides</a> 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. <a href="http://www.cl.cam.ac.uk/~jrh13/atp/index.html" rel="nofollow">Example code</a> is available online.</p>

<p>Philipp Ruemmer's <a href="http://www.philipp.ruemmer.org/princess.shtml" rel="nofollow">Princess</a> 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. </p>

CC BY-SA 3.0
2011-09-02T02:50:00.467Z
2011-09-02T02:57:14.560Z
2011-09-02T02:57:14.560Z
Vijay D
<p>What about tools, if you decide to you Prolog as language of choice, I can suggest a few implementation approaches :</p>

<ul>
<li><a href="http://www.gprolog.org/" rel="nofollow noreferrer">GNU Prolog</a> 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 <a href="https://stackoverflow.com/questions/7151675/prolog-compatibility-layers-available-programming-libraries">Prolog compatibility layers @SO</a></li>
<li><a href="http://www.swi-prolog.org/" rel="nofollow noreferrer">SWI-Prolog</a> has interesting programming library, including network communication, Protocol Buffers Support etc. And is quite popular.</li>
<li><a href="http://xsb.sourceforge.net/" rel="nofollow noreferrer">XSB Prolog</a> some people claim it's most interesting project in terms of interoperability - including : databases interfaces etc.</li>
</ul>

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

CC BY-SA 3.0
2011-09-01T22:21:29.330Z
2011-09-01T22:21:29.330Z
2017-05-23T12:40:09.333Z
Grzegorz Wierzowiecki
<p>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.</p>

<p>Thus,
I'm interested in learning more about constraint satisfaction where the constraints have what I will call <em>external variables</em>, <em>predicates</em> and <em>functions</em>,
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 <em>open</em> (as constraints are not entirely known) or <em>interactive</em> (as interaction is required to proceed with constraint satisfaction).</p>

<p>I would like to know both:  </p>

<ul>
<li>theoretical research done in this direction</li>
<li>tools or libraries that implement constraint solvers that allow interaction with the external world during the constraint solving process.</li>
</ul>

<sat><lo.logic><csp>
Open or Interactive Constraint Satisfaction
Dave Clarke
# Open or Interactive Constraint Satisfaction

(Asked by: username_0 on 2010-10-19)

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.

**Tags:** sat, lo.logic, csp

---

## 5 answers

### Answer by username_1 on 2010-10-19. Score: 9

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

An attempt to study the tractability questions was:

* Martin J. Green and Christopher Jefferson, *Structural Tractability of Propagated Constraints*, CP 2008.
  doi: [10.1007/978-3-540-85958-1\_25](http://dx.doi.org/10.1007/978-3-540-85958-1_25)

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.

> **Comments:**
> **username_0**: That paper certainly looks interesting. I never thought of SMT solvers as doing what I require. It's certainly an avenue to explore.  
> **username_2**: 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.  
> **username_1**: @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ć (http://argo.matf.bg.ac.rs/publications/2010/alldiff-smt2010.pdf).  

---

### Answer by username_3 on 2010-10-21. Score: 7

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.


---

### Answer by username_4 on 2010-10-19. Score: 7

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](http://www.decision-procedures.org).

> **Comments:**
> **username_0**: 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.  
> **username_4**: @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.  
> **username_4**: @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).  
> **username_0**: I think Amazon is calling.  
> **username_4**: @Dave: OK, excellent! ;-)  

---

### Answer by username_2 on 2011-09-02. Score: 4

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](http://www.decision-procedures.org/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](http://www.cl.cam.ac.uk/~jrh13/atp/index.html) is available online.

Philipp Ruemmer's [Princess](http://www.philipp.ruemmer.org/princess.shtml) 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.


---

### Answer by username_5 on 2011-09-01. Score: 0

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

* [GNU Prolog](http://www.gprolog.org/) 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](https://stackoverflow.com/questions/7151675/prolog-compatibility-layers-available-programming-libraries)
* [SWI-Prolog](http://www.swi-prolog.org/) has interesting programming library, including network communication, Protocol Buffers Support etc. And is quite popular.
* [XSB Prolog](http://xsb.sourceforge.net/) 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).


---

