[SMT-COMP] SMT Solvers at the Open ASP Competition
Giovambattista Ianni
ianni at mat.unical.it
Fri Feb 4 12:44:00 EST 2011
Dear Aaron, Clark, Cesare, members of the list all,
I guess many of you received a personal invitation from me as chair of the Third
Open Answer Set Competition.
The spirit of the Model & Solve Track of this Competition is to collect
declarative language systems, belonging to neighboring communities, and compare
them on common grounds, so to increase the level of hosmosis between these and
understand similarities and point of strengths of each.
This year we will have, among participants, representatives from the Prolog/CHR
world, some PDDL planner, Answer Set Systems and a FO(ID) system.
Unfortunately, besides appreciation and interest, of which I kindly thanks,
we had no concrete joins from the SMT community.
I understand that most of you has currently no manpower for participating: the
satlib 2.0 is under hot development, as well as the new SMT Competition is coming.
Consider however that we do accept also symbolic participations, e.g.
participating in just a few representative problem domains in which SMT fits
better and performs well: we are absolutely not asking SMT systems to play on
unfair grounds.
We have for instance some scheduling problem, involving arithmetics, or classic
graph domains, such as colorability, and some planning problem.
I see that not all the SMT systems might fit: but all we require is a minimal
ability to work with quantified formulas, arithmetics, and the capability of
displaying what we neutrally call a 'witness' (in your case, a satisfying model
or a counterexample model).
As a proposal, you could have a look at the Benchmark suite,
https://www.mat.unical.it/aspcomp2011/OfficialProblemSuite
and check whether there are 1-2 problems of which you have already
specifications which can be easily adapted. We can help about writing pre and
post-processing scripts for input instances and output witnesses.
We do not expect that SMT systems tackle all the benchmarks, but it would be
great having selected representatives of the community competing and being
compared with other fields on longstanding traditional problems. The Competition
also makes all participants much more visible in neighbor areas, each of which
is often relatively closed to novelty coming from outside.
I see that you might have no time anyway, so I will not insist anymore if this
proposal does not fit, although I personally feel as a pity not having a
representative of the SMT world at this venue: and, as many of you requested, we
will keep your community informed about next open ASP competitions.
(last remark: deadline is set to 25th of February but subject to further
important shifts)
with regards, GB
More information about the SMT-COMP
mailing list