Discussion Topics
In the discussion sessions on Friday afternoon, we can discuss any topic that has come up during the meeting. Some potential topics that are of interest are:
"The Proper Treatment of Undefinedness in Constraint Languages"
(proposed by Allan Frisch)
The goal is to address the problem of undefined expressions in constraint languages. Several alternative semantics for a simple constraint language that has undefined expressions will be discussed. It will be shown that for each of the semantics, models that contain undefined expressions can be translated to models that don't, while preserving satisfiability.
"Is SAT dead? Where is SAT research going with
increased ASP interest and industry funded SMT research."
(proposed by Daniel LeBerre)
SAT has be very successful in the beginning of 2000 because of its use in EDA. The SAT solvers have been increasingly fast and robust. However, now hardware and software verification community has a clear preference for SMT solvers. ASP solvers are now reaching SAT solvers efficiency with additional features appealing for people from AI. On the other hand, SAT solvers are the backbone of the SMT solvers. ASP solvers inherit many features from SAT solvers. Most improvements in SAT have direct benefit on SMT, maybe ASP. And what about Chaff patent threat (see SAT Live!) for the future of practical SAT/ASP/SMT research?
"Bridging the gap between ASP and SAT: the road via
FO(ID)."
(proposed by Marc Denecker)
Despite considerable difference in terminology, the ASP language and FO(ID) are extremely similar in use. This requires some explanation. An argument for integration.
"Computing structures from specifications: a new field for CP, ASP
and SAT research?"
(proposed by David Mitchell)
For one community "constraint modelling languages" is the obvious answer; for some researchers "answer set programming" is the answer (even when no stable models are involved), etc. There are several other groups doing much the same work under no special name. To build a community on the commonality of these, we should start using a common term.
"Applications: constraint-based methods for bioinformatics"
(proposed by Agostino Dovier)
Biology is a strong source of challenging applications for CP, ASP, and SAT techniques. Confer the workshops WCB (on constraint-based methods for bioinformatics) - this year it was colocated with CPAIOR. See also a special issue of "Constraints" on this material: http://ai.uwaterloo.ca/~vanbeek/Constraints/vol13.html
"How to make more intelligent grounders?"
(proposed by Marc Denecker)
SAT people write C programs to create CNF theories. In ASP and elsewhere, grounders are used to turn a KR theory into a propositional theory. Developing more intelligent grounders is an active research domain in these areas. How big is the gap? How far are grounders behind humans in creating good and fast propositional encodings? What are the challenges? What kind of techniques are needed to make more intelligent grounders that create smaller and better groundings? Related, what are techniques for tuning an encoding in SAT, ASP or CP, to get the problem solved, and is there any chance that these could be automated?
