[SMT-LIB] How can a SMT Solver fit for the Open ASP Competition?

[Giovambattista Ianni]

Dear members of the list,

I guess many of you received a personal invitation from me as chair of the Third 
Open Answer Set Competition or has heard about the ASP 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.

*******************************************************************************
Worth clarifying that the declarative language in which to implement problem 
domains is *open*: it is not necessary a translator from ASP theories to SMT-LIB 
encodings, *nor any knowledge of Answer Set Programming*.
*******************************************************************************

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.

Some explanation on how the Model & Solve track of the competition works: 
basically each participant has to model a series of problem domains in his 
declarative language of choice. Such problem specifications are then coupled 
with problem instances and evaluated, so to measure performance.
---------------------------------

*** Participating in practice ***

The file formats involved in the "Model and Solve Track" are three, 2 of which 
very simple and trivial to parse/convert. Take the 3-colorability problem as an 
example.

1. Input instance file format. These are just a set of logic ground facts to be 
taken as assertions, like 'node(a). edge(a,c). ..', which encode the graph at 
hand, of which we want to prove, say, 3-colorability.
The above, in SMT-LIB would correspond to FO ground atoms referring to 
predicates, or, in the terminology of SMT-LIB 2.0, are assertions regarding the 
codomain of boolean functions.

2. Problem specification format. This one is open and can be written in *any* 
declarative language format: it could be written in SMT-LIB or PDDL for 
instance. All we need is just a theory expressed in the predicate vocabulary of 
the input instance, extended with the vocabulary of output (or a syntactic 
conversion of these).
In the case of 3-colorabilities, anything enforcing, in the semantic of the 
language of choice, a predicate col(node,color) to describe a 3-colorability for 
the graph described by the input instance file, would serve the job:

In unsorted FO-like syntax (with unique names assumption) I would write this 
similar to

\forall x,y,c1,c2 ( edge(x,y) \and color(c1) \and color(c2) ) -> ( col(x,c1) 
\and col(y,c2) \and c1 != c2 )

(modulo additions for enforcing the domain of 'color' to three labels, say, r,g 
and b)
a model of the above (conjuncted with the input assertions), properly polished, 
would encode a 'witness' of 3-colorability.

Some of the SMT-LIB logics like AUFLIA are, in principle, suitable for the 
purpose of specifying problem domains, while I would exclude quantifier free 
logics: I see that these SMT logics have been used e.g. for scheduling problems, 
but I also see that problem instances, like those of the scheduling domain, come 
already grounded, as it is similarly done for SAT benchmarks.

We look for frameworks in which problems can be specified at an higher level of 
abstraction (at the, say, non-ground level): the competition is not suitable for 
SAT solvers, since these rarely focussed in their longstanding history on 
converting problems and their instances to propositional theories on the basis 
of a declarative specification.

3. output solution format. For each instance file we ask for a 'witness', e.g. a 
solution. For the example above, this is a set of assertions in the form 
'col(node,color)' describing a valid 3-colorability for the input graph at hand.
This can come from a projection of a model (or a counter-model) depending on how 
the logical specification at point (2) is given.

Assuming writing a generic spec of the problem for point (2) is possible, one 
thus need some scripting for turning the simple format of (1) into SMT-LIB and 
some similar post-processing for obtaining an output for point (3).

I see that not all the SMT systems might fit: but all that is required, for 
specifying problems in our benchmark suite, 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).
-------------------------------------------------

**** LAST CALL ****

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.


Deadline is set to 15th of March. More Info:

http://aspcomp2011.mat.unical.it

with regards, GB