INF Category

The INF category deals with 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 == term

has 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

1. (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 is YES.

2. (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 YES.

3. (PROBLEM INFEASIBILITY)
   (CONDITIONTYPE ORIENTED)
   (VAR x y)
   (RULES
     f(x) -> g(x)
   )
   (CONDITION f(x) == g(y))
   (COMMENT ill-formed)
   

   This inlined problem is ill-formed. Since there is a no (VAR idlist) declaration before the condition, x and y are constants in the condition but also variables in the TRS, which is forbidden.

Supporting Tools

• inlining tool for infeasibility problems

Problem Selection

Problems are selected among those in COPS with the 'infeasibility' tag.