Pseudo-Boolean Evaluation 2006: 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/02/20

Revisions of this document



Registering the solver to the right category

As explained in the section on the input format (see below), benchmarks may contain arbitrarily long integers that don't fit in a usual 32-bits integer. The page on integer overflows explain 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, three categories are defined
Two other categories are defined:

Incomplete solvers

Incomplete solvers are 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.
Submitters must indicate is their solver is complete or incomplete on the submission form.

Execution environment

The 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,...)

The pseudo-Boolean solver must accept one first parameter which is the name of the file containing the pseudo-Boolean instance, and a second parameter, which is a number between 0 and 4294967295 to be used as a seed for the random generator if the solver uses random numbers:
	./mysolver instancefile.pb 12345
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).

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

After PBTIMEOUT 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 file format is a  stricter variant of the OPB format (see the end of the README file in Here is an example:

* #variable= 5 #constraint= 4
* comments
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 ;
Most of the syntax of this file can be described by a simple BNF grammar (see <formula> is the start symbol of this grammar.
<formula>::= <sequence_of_comments>

<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>]

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

<linearfunction>::= <product> | <product><linearfunction>
<product>::= <integer> <oneOrMoreSpace> <variablename> <oneOrMoreSpace>

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

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

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

<oneOrMoreSpace>::= " " [<oneOrMoreSpace>]
<zeroOrMoreSpace>::= [" " <zeroOrMoreSpace>]
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

The solvers must output messages on the standard output that 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.


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

If the solver does not output a solution line, or if the solution line is misspelled, then UNKNOWN will be assumed.

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.