Participant submission procedure

Application

Teams willing to register to the competition can send an email to this address specifying:

• the name of their team;
• names and affiliation of the participants (institution, research group);

• whether the team will participate to the System or to the Model & Solve competition, or both.

You will get a private e-mail with credentials for accessing our Competition server through ssh. As soon as you will login the Competition server, you will find a Linux home directory having a folder structure described next. A sample home directory tree can be found here.

Instructions for testing and submitting systems and benchmarks

Your home directory in the Competition server contains a subdirectory submitted. Only files in this directory will be processed during the Competition. The content of the submitted directory depends on whether your team is participating to the system or model competition.

IMPORTANT: The submitted directory is readable but not directly writable, and should be used only for submitting systems and problem encodings in their final submitted version. Participants are provided with a try directory, structured as submitted. This directory can be used for testing systems and benchmark encodings.

Model & Solve Competition

If your team is participating to the model competition, your submitted directory will contain a subdirectory for each benchmark: let us call one of such directories benchmark_example. Each of these directories must include all files required for solving a specific benchmark. In particular, there must be an executable file named run, which will be invoked during the Competition. This file can be a script invoking a binary executable, possibly using other scripts for pre- or post-processing.

Take note that benchmark_example must be self-contained, thus:

• All files invoked/used by run must be placed in the directory containing the run file, or in one of its subdirectories;

• Except for system-wide available dynamic libraries and commands, all other file resources should be referred using paths relative to "." in all the scripts: note that this is a strong requirement, since the Competition will be executed on several machines (with same hardware, configuration and installed libraries) and in an environment different from your home directory;

• If you rely on a particular value of the $PATH variable please set this on your run script; $PATH can anyway list only system folders and relative paths in your submitted directory.

• Note that if you're using the same system binary for all the benchmark problems you will have to make a copy of it on each benchmark directory.

{{{run}}} command line syntax

During the Competition, the run file will be invoked with two command-line arguments. The first argument is the maximum integer which is sufficient for solving the input instance. The second argument is the maximum nesting level of function symbols which is sufficient for solving the input instance. These arguments can be passed to the binary executable or just ignored. Instances will be provided via standard input. The output must be printed in standard output, according to the format specified in the benchmark description. Examples of scripts will be provided in each benchmark directory. Below is an example of run script.

# !/usr/bin/env bash

set -o pipefail     # Disable output buffering

if [ $# -ne 2 ]; then
    echo "This script must be invoked with two parameters!"
    exit -1
fi

MAXINT=$1
MAX_NESTING_LEVEL=$2    # NOTE: MAX_NESTING_LEVEL is not used in this version of DLV

SCRIPTDIR=`dirname $0`
BIN=$SCRIPTDIR/dlv.i386-linux-elf-static.bin
ENCODING=$SCRIPTDIR/myProblem1.dl
OUTPUT_PREDICATES=path

# Execution with preprocessing and postprocessing:
$SCRIPTDIR/preprocess.pl | $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent $ENCODING -- | $SCRIPTDIR/postprocess.pl

ECODE=$?
if [ $ECODE -ne 0 ]; then
    echo UNKNOWN;
fi
exit $ECODE

Note that, in the above script, DLV is invoked after a pre-processing perl script. The output of DLV is processed by a perl post-processing script. Your binary executable might not require a pre-processing script, in which case the following instruction can be used in the script:

# Execution with postprocessing only:
$BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent $ENCODING -- | $SCRIPTDIR/postprocess.pl

Similarly, if your binary executable does not require a post-processing script, the following instruction can be used in the script:

# Execution with preprocessing only:
$SCRIPTDIR/preprocess.pl | $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent $ENCODING --

System Competition

If your team is participating to the model competition, your submitted directory contains a subdirectory System. This directory must comprise all files required for running your system. In particular, there must be a file run, which will be invoked during the Competition. This file can be a script invoking a binary executable, possibly using other scripts for pre- or post-processing. All files invoked by run must be placed in the directory containing the run file, or in one of its subdirectories. Moreover, only relative paths must be used in all scripts; note that this is a strong requirement, since the Competition would be executed on a different machine. During the Competition, the run file will be invoked with three command-line arguments. The first argument is the maximum integer which is sufficient for solving the input instance. The second argument is the maximum nesting level of function symbols which is sufficient for solving the input instance. The third argument will be specified in the command-line, which will be a comma-separated list of predicate names. These predicates must be used for representing witnessing models of satisfiable instances; the extensions of these predicates must be printed in standard output. Each of these arguments can be passed to the binary executable or just ignored. Instances will be provided via standard input. The output must be printed in standard output, according to the format specified in the benchmark description. Examples of scripts will be provided in the System directory. Below is an example of run script.

# !/usr/bin/env bash

set -o pipefail     # Disable output buffering

if [ $# -ne 3 ]; then
    echo "This script must be invoked with three parameters!"
    exit
fi

MAXINT=$1
MAX_NESTING_LEVEL=$2    # NOTE: MAX_NESTING_LEVEL is not used in this version of DLV
OUTPUT_PREDICATES=$3

SCRIPTDIR=`dirname $0`
BIN=$SCRIPTDIR/dlv.i386-linux-elf-static.bin

# Execution with preprocessing and postprocessing:
$SCRIPTDIR/preprocess.pl | $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent -- | $SCRIPTDIR/postprocess.pl

ECODE=$?
if [ $ECODE -ne 0 ]; then
    echo UNKNOWN;
fi
exit $ECODE

Note that, in the above script, DLV is invoked after a pre-processing perl script. The output of DLV is processed by a perl post-processing script. Your binary executable might not require a pre-processing script, in which case the following instruction can be used in the script:

# Execution with postprocessing only:
$BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent -- | $SCRIPTDIR/postprocess.pl

Similarly, if your binary executable does not require a post-processing script, the following instruction can be used in the script:

# Execution with preprocessing only:
$SCRIPTDIR/preprocess.pl | $BIN -N=$MAXINT -filter=$OUTPUT_PREDICATES -n=1 -silent --

Submission Process

The submission process will be performed by properly invoking the submit tool. This tool requires a command-line parameter specifying either System or the name of a directory containing a benchmark solution (just the name, not the complete path). Once a system or a benchmark are submitted, any modification to the associated directories is prevented. At any time, a participant can invoke the unsubmit tool to retire a submitted directory and get back the grant of modifying its content.

Examples

To submit your System directory, just write:

$ submit System

The System directory will be no more editable. To undo your submission, type:

$ unsubmit System