Open or Interactive Constraint Satisfaction 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.
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


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.