[SMT-COMP] SMT Solvers at the Open ASP Competition

[Giovambattista Ianni]

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