CoCo 2019 will feature a new competition category on infeasibility problems.
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
numberrefers 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
->*). Variables declared in
idlistare used as variables in
(VAR idlist)declaration can be omitted if the terms in
condlistare ground. Common function symbols occurring in COPS ♯
condlisthave the same arity. Moreover, function symbols in COPS ♯
numberdo not occur as variables in
idlistand function symbols in
condlistdo not occur as variables in COPS ♯
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
(CONDITION condlist) is
YES if no satisfying substitution exists,
NO if a satisfying substitution exists.
(PROBLEM INFEASIBILITY) (COPS 547) (VAR x) (CONDITION x == a, x == b) (COMMENT doi:10.4230/LIPIcs.FSCD.2016.29  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 is
(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 is
Problems are selected among those in COPS with the 'infeasibility' tag.