News

• 26/5: A clarification on the Reachability checker : The input to this checker should consist of the instance followed by the witness. The order is important, otherwise the checker will fail.
  
  
• 26/5: A clarification on Reachability: The reachability relation is the transitive closure of the edge relation, and hence not by definition reflexive! A reflextive tuple (x,x) belongs to it, only if there is a non-empty path from x to x.
  
  
• 22/5: A clarification on Weight Bounded Dominating Set: Note that instances may contain atoms of "edgewt" that do not correspond to atoms of "edge".
  
  
• 22/5: A clarification on Grammar-Based Information Extraction: if the equation in an instance is not satisfied, the instance should be UNSATISFIABLE (rather than have the empty witness as originally stated on the webpage)..
  
  
• 22/5: Today, the competition database will be reinitialized with the compeitition instances. During a short period, the submission and check scripts will not be operational. After this, you still have a few days to submit or resubmit solutions for benchmarks.
  
  
• 22/5: If your solver finds the empty witness, it should output a newline character!
  
  
• 19/5: Run the script check-submissions to test the status of all your contributions.
  
  
• 15/5: Policy in case of errors:
  
  

  Recall that giving an incorrect answer disqualifies a solver for all instances of a benchmark! In particular, take care that your script does not return "UNSATISFIABLE" per default, e.g., in case of a time-out or of an error of your solver. "UNSATISFIABLE" should be returned only when your solver established unsatisfiability of the instance.

  Please check your encapsulating scripts. For instance, if a solver would usually output a witness for a positive answer in a line starting with "Stable Model: " or write "False" in case of a negative answer, an encapsulating script like the one below can lead to unexpected "UNSATISFIABLE" answers and possibly to disqualification:
  IF "Stable Model: <witness>" THEN print "<witness>"
  ELSE print "UNSATISFIABLE"

  In such a case, a script should roughly look as follows:
  IF "Stable Model: <witness>" THEN print "<witness>"
  ELSEIF "False" THEN print "UNSATISFIABLE"
  ELSE print "UNKNOWN"
  

• 12/05: Clarification on Reachability:
  
  The output format is now described more accurately.
  
  
• 12/05: Submissions:
  
  Added a note about static vs. dynamically linked libraries. We encourage all entrants to use statically linked libraries in their solver builds.
  
  
• 12/05: Clarification on Labyrinth:
  
  The problem description mistakenly referred to the predicate max_step, when max_steps was intended.
  
  
• 11/05: Clarification on Hanoi:
  
  the action of moving a tile to its original place has no effect. However, such dummy actions are not needed to solve the competition instances.
  
  
• 11/05: Clarification on Sokoban:
  
  In this planning problem, the action of pushing a block to its current position has no effect. Yet, since one push action is needed per time point, such dummy actions may be necessary to solve certain instances of the competition!
  
  
• 11/05: Clarification on EdgeMatching :
  
  the problem description mistakenly referred to chosePosition, where chosenTile was meant. This was corrected.