Benchmark Problem Classification
Problems, on which systems will compete, are classified according to type, complexity and language. Such categorizations are independent, although strictly related each other.
We herein adopt witness as a neutral term for denoting a solution for the given problem instance. Depending on the declarative formalism of choice, this can correspond to (part of) a logical model, to a satisfying assignment, etc. In ASP terminology, a witness corresponds to an answer set or a subset thereof.
We distinguish between the following types of problems:
Optimization problems, and
The first type of problem requires to find (if it exists) a "witness" solving the problem instance at hand (e.g. a coloring for a given instance graph).
An optimization problem is specified as a search problem together with a cost function which assigns an integer cost value to witnesses. We are always searching for witnesses with minimal cost.
A query problem consists in finding all the facts (having a given signature) which hold in all the "witnesses" of the instance for the problem at hand. Query problems include decision problems in which an answer can be a boolean value (e.g. deciding satisfiability of a given propositional formula).
Problems are also classified according to their computational complexity in:
Polynomial problems: We classify in this category problems which are solvable in polynomial time in the size of the input data (data complexity). Such problems are usually characterized by the huge size of instance data.
NP problems: We classify in this category NP-complete problems and any problem in NP not known to be polynomially solvable. More precisely, we classify as NP all search problems in which witnesses correspond to polynomially checkable certificates of some NP-complete problem.
Beyond NP: We classify in this category any other problem not falling in the above. This class often includes, but it is not restricted to nontrivial optimization problems.
For problems accepted in the System Track benchmark problems are classified according to the language fragment used in the proposed/available encodings. A detailed specification of the language fragments is forthcoming.