Confluence Competition

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 == 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. The (VAR idlist) declaration can be omitted if the terms in condlist are ground. 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.

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.

Supporting Tools

Problem Selection

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