Pseudo-Boolean Evaluation 2007: requirements for solvers

This document lists the requirements that a solver must conform to. These requirements may evolve slightly over time. You're invited to check the content of this page regularly. The revisions of this document are detailed below.

Last modification: 2006-10-30 (YYYY-MM-DD format)

Revisions of this document

Major

Minor

Registering the solver to the right category

Because not all solvers are able to solve every kind of instances, you will be asked when you register your solver to indicate which category of benchmarks it is able to handle. This year, we have up to 8 categories defined by the ability of the solver to
Two categories are defined based on the presence of an objective function or not:
Two categories are defined based on the kind of contraints contained in the instance:
As explained in the section on the input format (see below), benchmarks may contain arbitrarily long integers that do not fit in a usual 32-bits integer. The page on integer overflows explains why we consider that a strong solver should use a multiple precision integer library. However, we do not require that you modify your existing solver to use big integers. We just need that you register your solver in the categories which it is able to solve. This is an important decision because registering a solver in a given category is a claim that it will give correct answers for each benchmark in that category.

Concerning the integers values, two categories are defined

Complete and incomplete solvers

Complete solvers are solvers which can always decide if the formula is satisfiable or not, provided they are given enough time and memory. Incomplete solvers are able to give some answers (SAT/UNSAT) but not all. They may loop endlessly in a number of cases. Local search algorithms are examples of incomplete solvers. There is a high probability that they find a solution if the instance is satisfiable, but they will not be able to prove unsatisfiability.

Both kinds of solvers are welcome in this evaluation. Submitters will have to indicate if their solver is complete or incomplete on the submission form.

Complete solvers

There is no special requirement about complete solvers. See the input and output format that all solvers must respect for details.

Incomplete solvers

Incomplete solvers are definitely welcome in this evaluation. Despite the fact that they will never answer UNSATISFIABLE or OPTIMUM FOUND, incomplete solvers can be registered in both the SAT/UNSAT and OPT categories.

In the SAT/UNSAT category, an incomplete solver will stop as soon as it finds a solution and will time out if it can't find one. The only difference with a complete solver is that it will time out systematically on unsatisfiable instances.

In the optimisation category, an incomplete solver will systematically time out because it will be unable to prove that it has found the optimum solution. Yet, it may have found the optimum value well before the time out. In order to get relevant informations in this category, an incomplete solver must fulfill two requirements:
  1. it must intercept the SIGTERM sent to the solver on timeout and output either "s UNKNOWN" or "s SATISFIABLE" with the "v " line corresponding to the best model it has found
  2. it MUST output "o " lines whenever it finds a better solution so that, even if the solver always timeout, the timestamp of the last "o " line indicates when the best solution was found. Keep in mind that it is the evaluation environment which is in charge of timestamping "o " lines.

Execution environment

Solvers will run on a cluster of computers using the Linux operating system. They will run under the control of another program (runsolver) which will enforce some limits on the memory and the total CPU time used by the program. Solvers will be run inside a sandbox that will prevent unauthorized use of the system (network connections, file creation outside the allowed directory, among others).

All solvers will be run as a 32 bits application. Therefore, if you submit an executable, you are required to provide us with a 32 bit ELF executable (preferably statically linked). Solvers submitted in source form will be compiled on a 32 bit platform.

Two executions of a solver with the same parameters and system resources must output the same result in approximately the same time (so that the experiments can be repeated).

During the submission process, you will be asked to provide the organizers with a suggested command line that should be used to run your solver. In this command line, you will be asked to use the following placeholders, which will be replaced by the actual informations by the evaluation environment.
Examples of command lines:
	DIR/mysolver BENCHNAME RANDOMSEED
DIR/mysolver --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --tmpdir=TMPDIR BENCHNAME
java -jar DIR/mysolver.jar -c DIR/mysolver.conf BENCHNAME
As an example, these command lines could be expanded  by the evaluation environment as
	/solver10/mysolver file.pb 1720968
/solver10/mysolver --mem-limit=900 --time-limit=1200 --tmpdir=/tmp/job12345 file.pb
java -jar /solver10/mysolver.jar -c /solver10/mysolver.conf file.pb
The command line provided by the submitter is only a suggested command line. Organizers may have to modify this command line (e.g. memory limits of the Java Virtual Machine (JVM) may have to be modified to cope with the actual memory limits).

The solver may also (optionally) use the values of the following environment variables:

After TIMEOUT seconds have elapsed, the solver will first receive a SIGTERM to give it a chance to output the best solution it found so far (in the case of an optimizing solver). One second later, the program will receive a SIGKILL signal from the controlling program to terminate the solver.

The solver cannot write to any file except standard output, standard error and files in the TMPDIR directory. A solver is not allowed to open any network connection or launch unexpected external commands. Solvers may use several processes or threads.

Input Format

The input format for this year's evaluation is a generalization of the previous format in order to allow the specification of non-linear pseudo-Boolean instances. Nevertheless, linear pseudo-Boolean instances will comply with the PB06 input format.

As in the PB06 evaluation, the input file format for pseudo-Boolean instances is maintained as a stricter variant of the OPB format (see the end of the README file in http://www.mpi-sb.mpg.de/units/ag2/software/opbdp/opbdp1.1.1.tar.gz). For linear pseudo-Boolean instances, the file format is exactly the same as in the PB06 evaluation. For non-linear pseudo-Boolean instances, a generalization of this format is proposed with the following changes:

With these generalizations, it is possible to specify constraints like:

3 x1 x2 + 2 ~x3 ~x4 ~x5 -3 x6 >= +2 ;
If we would not allow negative literals in the format, we would have to replace the term
2 ~x3 ~x4 ~x5
with the following expression
-2 x3 -2 x4 -2 x5 +2 x3 x4 +2 x3 x5 +2 x4 x5 -2 x3 x4 x5 +2

Here are a few examples:

Linear instances (same format as in the PB06 evaluation)
Non-linear instances (extension of the PB06 format)
* #variable= 5 #constraint= 4
*
* this is a dummy instance
*
min: 1 x2 -1 x3 ;
1 x1 +4 x2 -2 x5 >= 2;
-1 x1 +4 x2 -2 x5 >= +3;
12345678901234567890 x4 +4 x3 >= 10;

* an equality constraint
2 x2 +3 x4 +2 x1 +3 x5 = 5;
* #variable= 5 #constraint= 4 #product= 5 sizeproduct= 13
*
* this is a dummy instance
*
min: 1 x2 x3 -1 x3 ;
1 x1 +4 x1 ~x2 -2 x5 >=2;
-1 x1 +4 x2 -2 x5 >= 3;
12345678901234567890 x4 +4 x3 >= 10;
2 x2 x3 +3 x4 ~x5 +2 ~x1 x2 +3 ~x1 x2 x3 ~x4 ~x5 = 5 ;
* #variable= 15 #constraint= 21
*
* linearized version of the factorization problem (P*Q=35)
* this linearization can be automatically done by the parsers we provide
min: +1 x1 +2 x2 +4 x3;
+1 x1 +2 x2 +4 x3 >= 2;
+1 x4 +2 x5 +4 x6 >= 2;
+1 x7 +2 x8 +4 x9 +2 x10 +4 x11 +8 x12 +4 x13 +8 x14 +16 x15 = 35;
* new variables introduced to represent the products
+1 x7 -1 x1 -1 x4 >= -1;
-2 x7 +1 x1 +1 x4 >= 0;
+1 x8 -1 x1 -1 x5 >= -1;
-2 x8 +1 x1 +1 x5 >= 0;
+1 x9 -1 x1 -1 x6 >= -1;
-2 x9 +1 x1 +1 x6 >= 0;
+1 x10 -1 x2 -1 x4 >= -1;
-2 x10 +1 x2 +1 x4 >= 0;
+1 x11 -1 x2 -1 x5 >= -1;
-2 x11 +1 x2 +1 x5 >= 0;
+1 x12 -1 x2 -1 x6 >= -1;
-2 x12 +1 x2 +1 x6 >= 0;
+1 x13 -1 x3 -1 x4 >= -1;
-2 x13 +1 x3 +1 x4 >= 0;
+1 x14 -1 x3 -1 x5 >= -1;
-2 x14 +1 x3 +1 x5 >= 0;
+1 x15 -1 x3 -1 x6 >= -1;
-2 x15 +1 x3 +1 x6 >= 0;

* #variable= 6 #constraint= 3 #product= 9 sizeproduct= 18
*
* Factorization problem: find the smallest P such that P*Q=N
* P is a 3 bits number (x3 x2 x1)
* Q is a 3 bits number (x6 x5 x4)
* N=35
*
* minimize the value of P
min: +1 x1 +2 x2 +4 x3 ;
* P>=2 (to avoid trivial factorization)
+1 x1 +2 x2 +4 x3 >= 2 ;
* Q>=2 (to avoid trivial factorization)
+1 x4 +2 x5 +4 x6 >= 2 ;
* P*Q=N
+1 x1 x4 +2 x1 x5 +4 x1 x6 +2 x2 x4 +4 x2 x5 +8 x2 x6 +4 x3 x4 +8 x3 x5 +16 x3 x6 = 35;

The syntax of the input file format can be described by a simple BNF grammar (see http://en.wikipedia.org/wiki/Backus-Naur_form). <formula> is the start symbol of this grammar.

<formula>::= <sequence_of_comments>
[<objective>]
<sequence_of_comments_or_constraints>

<sequence_of_comments>::= <comment> [<sequence_of_comments>]
<comment>::= "*" <any_sequence_of_characters_other_than_EOL> <EOL>
<sequence_of_comments_or_constraints>::=<comment_or_constraint> [<sequence_of_comments_or_constraints>]
<comment_or_constraint>::=<comment>|<constraint>

<objective>::= "min:" <zeroOrMoreSpace> <sum> ";"
<constraint>::= <sum> <relational_operator> <zeroOrMoreSpace> <integer> <zeroOrMoreSpace> ";"

<sum>::= <weightedterm> | <weightedterm> <sum>
<weightedterm>::= <integer> <oneOrMoreSpace> <term> <oneOrMoreSpace>

<integer>::= <unsigned_integer> | "+" <unsigned_integer> | "-" <unsigned_integer>
<unsigned_integer>::= <digit> | <digit><unsigned_integer>

<relational_operator>::= ">=" | "="

<variablename>::= "x" <unsigned_integer>

<oneOrMoreSpace>::= " " [<oneOrMoreSpace>]
<zeroOrMoreSpace>::= [" " <zeroOrMoreSpace>]
For linear pseudo-Boolean instances, <term> is defined as
<term>::=<variablename>
For non-linear instances, <term> is defined as
<term>::= <oneOrMoreLiterals>
<oneOrMoreLiterals>::= <literal> | <literal> <oneOrMoreSpace> <oneOrMoreLiterals>
<literal>::= <variablename> | "~"<variablename>

Some comments and details:
Notice that integers may be of arbitrary size in the file. See here for a rationale.

The rules let us write a very simple parser and avoid some ambiguities present in the original description of the OPB format. At the same time, the format remains easily human readable and is compatible with solvers using the OPB format.

Output Format

Solvers must output messages to the standard output and those messages will be used to check the results. The output format is inspired by the DIMACS output specification of the SAT competition and may be used to manually check some results.

Messages

With the exception of the "o " line, there is no specific order in the solvers output lines. However, all lines, according to its first char, must belong to one of the four following categories:

Bugs and wrong answers...

A solver is declared to give a wrong answer in the following cases: When a solver provides even one single wrong answer in a given category of benchmarks, the solver's results in that category will be excluded from the final evaluation results because they cannot be trusted. Exceptionally, the organizers may decide to present separately the results of such a solver but only if it obtained particularly good results and if a detailed explanation of the problem as well as a solution is provided by the submitters.

A solver which ends without giving any solution, or just crashes for some reason (internal bugs...), is simply considered as giving an UNKNOWN result. It is buggy, but not incorrect.