Infeasibility Category
CoCo 2019 will feature a new competition category on infeasibility problems.
Format
Infeasibility problems are incorporated into COPS as follows:
(PROBLEM INFEASIBILITY) (COPS number) (VAR idlist) (CONDITION condlist) (COMMENT string)where
condlist ::= cond  cond , condlist cond ::= term == termhas the same syntax as the conditional part of a conditional rewrite rule and
number
refers to an existing problem in CTRS
or TRS format. If it is a CTRS then the semantics of ==
is
the same as declared in the (CONDITIONTYPE ctype)
declaration of the CTRS; if it is a TRS then the semantics of
==
is ORIENTED
(>*
). Variables declared in idlist
are used as variables in condlist
.
Common function symbols occurring in COPS
♯number
and condlist
have the same arity.
Moreover, function symbols in COPS ♯number
do not occur as variables in idlist
and function
symbols in condlist
do not occur as variables in
COPS ♯number
. The
(VAR idlist)
declaration can be omitted if the terms in condlist
are ground.
For the competition, the (COPS number)
declaration
will be inlined, before the problem is passed to participating tools.
The inlining program is available.
The question to be answered is whether
condlist
in
(CONDITION condlist)
is
infeasible: YES
if no satisfying substitution exists,
NO
if a satisfying substitution exists.
Examples

(PROBLEM INFEASIBILITY) (COPS 547) (VAR x) (CONDITION x == a, x == b) (COMMENT doi:10.4230/LIPIcs.FSCD.2016.29 [90] Example 3 submitted by: Raul Gutierrez and Salvador Lucas )
which expands to(PROBLEM INFEASIBILITY) (COMMENT COPS 547) (CONDITIONTYPE ORIENTED) (VAR x) (RULES f(x) > a  x == a f(x) > b  x == b ) (VAR x) (CONDITION x == a, x == b)
The correct answer isYES
. 
(PROBLEM INFEASIBILITY) (COPS 47) (CONDITION G(A) == A) (COMMENT this comment will be removed)
which expands to(PROBLEM INFEASIBILITY) (COMMENT COPS 47) (VAR x) (RULES F(x,x) > A G(x) > F(x,G(x)) C > G(C) ) (CONDITION G(A) == A)
The correct answer isYES
. 
(PROBLEM INFEASIBILITY) (CONDITIONTYPE ORIENTED) (VAR x y) (RULES f(x) > g(x) ) (CONDITION f(x) == g(y)) (COMMENT illformed)
This inlined problem is illformed. Since there is a no(VAR idlist)
declaration before the condition,x
andy
are constants in the condition but also variables in the TRS, which is forbidden.
Supporting Tools
Problem Selection
Problems are selected among those in COPS with the 'infeasibility' tag.