Lambda the Ultimate

thanks

I'm wondering why the mozart/oz, gecode and the automated planning/theorem proving folks don't just interface to already created stuff, and why they don't use the that kind of terminology instead of saying walksat etc.

Also, are automated theorem proving/model checking (such as alloy), automated planning (strips satplan), and constraint programming basically the same thing invented in different places, or is their a real difference between them, if anyone knows. thanks

There are respects in which it makes sense to say that concurrent constraint programming, automated planning, and theorem proving are different. There are also respects in which it makes sense to say that they overlap. The term "WalkSAT" is used because that implementation's approach to the problem is stochastic, i.e. a form of random walk, as opposed to the complete DPLL approach to the problem.

Your overall point (to the extent that I understand it correctly) that a lot of these groups and efforts are talking past each other has a fair amount of merit. For better or worse, the domains of application of the various technologies in question tend to reinforce some of what would probably rightly be considered merely conceptual distinctions otherwise. For example, in some domains, the fact that an automated theorem prover for first-order logic might return "true," "false," or not return at all for any given statement is fine. For others, the fact that it might not ever return is categorically unacceptable, and the fact that you might not know whether it's going to return in a reasonable time or not likewise. That's where SAT solvers tend to come in.

Automated planning is a hard problem. SATPLAN is one way to tackle it. Linear Programming is another. The Event Calculus (the discrete flavor of which can be implemented in terms of SAT solving; cf. "Commonsense Reasoning") is another. And so on.

Finally, you may want to work with something more expressive than first-order logic, say something that's "strongly undecidable." At that point, you're looking at one of the interactive proof assistants such as Coq or Isabelle, and the question of automation effectively gets flipped on its head: there are a variety of decision procedures for fragments of the logic that are decidable, and that's nice. But most of your time will be spent, first figuring out how to say what you want to prove, and then using all of the tools at your disposal—and there are stacks and stacks of them—to build a proof that the proof checker will accept. If you're using one of the type-theory-based interactive proof assistants (Coq or Isabelle), then you can extract code that's "correct by construction" in one of the supported languages for extraction.

So yeah. There is a lot of conceptual overlap going on. But there are real differences, too, both conceptual and, even more so, pragmatic.

I'm wondering why the mozart/oz, gecode and the automated planning/theorem proving folks don't just interface to already created stuff, and why they don't use the that kind of terminology instead of saying walksat etc.

While WalkSat is a local search algorithm, constraint programming conducts a systematic search and uses various search algorithms (e.g., all solutions can be found, or even the best according to some user-defined criterion).

Different constraint programming languages/systems implement different approaches to search. Mozart/Oz and Gecode implement an approach to constraint programming that makes the search process itself programmable on a high level of abstraction (more specifically, they are based on the notion of computation spaces). Users can define, for example, their own dynamic variable and value orderings optimised for a specific class of problems, and they can program their own search engines. These definitions are independent of the actual constraint problem definition. This approach was developed by Christian Schulte for Oz and has been revised in the form of Gecode (which is a C++ library that a few other systems interface to). For details on this approach see his book Porgramming Constraint Services, where he also compares the performance of this approach (that uses copying) based on spaces with the traditional back-tracking based approach (that uses trailing; and is performed by Prolog implementations).

Hello Pkhuong,

Can you elaborate a bit more on what you don't like in Comet Language and what you would like to have to improve the language.
I use Comet every day and for me the syntax is very close from Java and C++ with very useful abstractions such as Closure, Aspect Programming, Continuations, Non-deterministic search control, Event-Programming.
Thank you in advance,

Pierre

In what context are you using Comet?

One paper:

Scalable Load Balancing in Nurse to Patient Assignment Problems:

Abstract. This paper considers the daily assignment of newborn infant patients to nurses in a hospital. The objective is to balance the workload of the nurses, while satisfying a variety of side constraints. Prior work proposed a MIP model for this problem, which unfortunately did not scale to large instances and only approximated the objective function, since minimizing the variance cannot be expressed in a linear model. This paper presents constraint programming (CP) models of increasing complexity to solve large instances with hundreds of patients and nurses in a few seconds using the Comet optimization system. The CP models use the recent spread global constraint to minimize the variance, as well as an exact decomposition technique.

Edit:

His Ph.D. thesis also uses COMET.

Solving Balancing and Bin-Packing problems with Constraint Programming

Edit #2: Holy smokes, Pierre. Your Ph.D. thesis has some amazing easter eggs.

Thanks. The paper indeed says that he is affiliated with dynadec.

First, I'll state that I think the domain specific technology behind COMET is really good stuff, and the brains behind it are really good at (mathematical) optimisation. I've had the pleasure of working with Laurent Michel in a workshop, and COMET was definitely very useful; however, I'm not sure how efficient we would have been without his guidance.

The language does not feel as if it'd been designed, nor planned. The manual indeed describes the syntax as being extremely close to C++ or Java... without any reference to a grammar definition. If I were to hazard a guess, I would say that the language was created by almagating things the designers (who are OR practitioners not PL theorists) liked in their previous experiences: Java, C++ and ML. That's how we get a manual that calls generic vectors "forall polymorphic". The restrictions on how types can be constructed probably reflect the simplicity of the original source-to-source compiler. Another restriction I don't understand is the lack of global variables or even class-allocated slots. I shouldn't have to thread state around...

The implementation itself isn't too hot. Never mind the fact that the continuations are implemented via stack-copying (the trick for sending them across boxen is nice though). Their new JIT targets GNU Lightning... the GCD of x86, PPC and SPARC doesn't leave a lot. Granted, if that is an issue, you're using COMET wrong.

Frankly, I don't understand why they didn't go with a better-known third-party language that's not too hard to embed into/bind with C. Lua, maybe Python, or Javascript (now) would work fine, and leave the developers to exploit their strength.

Hello,

I used Comet during my PhD and now I'm working for Dynadec.
Thank you very much for the feedback on Comet, it is very valuable for us.
My background is not on languages but rather on the algorithmic aspects of CP.
We are putting a lot of efforts currently to write documentation and user manuals such that you don't need guidance any more ;-)

Pierre