Pseudo Boolean Evaluation 2005: 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.

Last modification: 2005/04/22

Execution environment

The solvers will run on a cluster of standard PCs running under Linux.

Running the solver

The pseudo boolean solver must accept one single parameter which is the name of the file containing the pseudo boolean instance.

	./mysolver instancefile.pb
If a solver uses random numbers, it must accept a second seed parameter, where seed is a number between 0 and 4294967295, e.g.,
./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:

Those values can be read using traditional C functions:
/* Return the limit or:
-1 if the variable is not set
0 if there was a problem in atoi (variable isn't a number) */
int getPBlimit(char *name) {
char *value = getenv(name);

if (value == NULL)
return -1;

return atoi(value);

After PBTIMEOUT is 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 and standard error (only standard output will be parsed for results, but both
output and error will be memorized during the whole competition process, for all executions).

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= 3
* 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;
Most of the syntax of this file can be described by a simple BNF grammar (see
<unsigned_integer>::= <digit> | <digit><unsigned_integer>
<integer>::= <unsigned_integer> | "+" <unsigned_integer> | "-" <unsigned_integer>
<identifier>::= <letter_or_underscore>[<sequence_of_letters_or_digits_or_underscores>]
<relational_operator>::= ">=" | "="

<product>::= <integer> "*" <identifier> " "
<linearfunction>::= <product> | <product><linearfunction>
<constraint>::= <linearfunction> <relational_operator> <integer> ";"
<objective>::= "min:" <linearfunction> ";"

<comment>::= "*" <any_sequence_of_characters_other_than_EOL> <EOL>
Some comments and details:
You may have noticed that integers may be of arbitrary size in the file. Don't panic, most of the benchmarks will only use small integers (that fit in a 32 bit integer) and you're not required to modify your solver. 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.

Below, you will find links to simple parsers for this format. Note that these parsers have minimal features, are not optimized and shouldn't be used as such in an industrial strength solver. Furthermore, they have not been intensively tested yet. You may therefore expect some updated version one day or another.

Simple Parser (C language)
Simple Parser (C++ language)
Simple Parser (Java language)
A sample Makefile
A tiny test file

Benchmark files

A set of benchmarks conforming to the evaluation format is available here.

Output Format

We ask for the solvers to DISPLAY messages on the standard output that will be used to check the results and to RETURN EXIT CODE to be handled by the evaluation system. The output format is inspired by the DIMACS output specification of the SAT competition and may be used to manually check some results.


There is no specific order in the solvers output lines. However, all line, according to its first char, must belong to one of the three following categories:

Technically, the two first chars are important and must be strictly respected: scripts will use traditional grep commands to parse results (and at least to partition standard output).

If the solver does not display a solution line (or if the solution line is not valid), then UNKNOWN will be assumed.

Providing a model

If the solver outputs SATISFIABLE, it should provide a model (or an implicant) of the instance that will be used to check the correctness of the answer. I.e., it must provide a list of non-contradictory literals that makes every constraint of the input formula true. When optimization is considered, this set of literals should give the minimum value of the utility function that the solver was able to discover. The negation of a literal is denoted by a minus sign immediately followed by the identifier of the variable. This solution line MUST define the value of EACH VARIABLE. The order of literals does not matter. Arbitrary white space characters, including ordinary white spaces, newline and tabulation characters, are allowed between the literals, as long as each line containing the literals is a values line, i.e. it begins with the two chars "v ".

Note that we do not require a proof for unsatisfiability. The values lines should only appear with SATISFIABLE instance (including instances for which an OPTIMUM was FOUND).

For instance, the following outputs are valid for the instances given in example:

mycomputer:~$ ./mysolver myinstance-sat
c mysolver 6.55957 starting with PBTIMEOUT fixed to 1000s
c Trying to guess a solution...
v x1 x2 -x5 x4 -x3
c Done (mycputime is 234s).

mycomputer:~$ ./mysolver myinstance-unsat
c mysolver 6.55957 starting with PBTIMEOUT fixed to 1000s
c Trying to guess a solution...
c Contradiction found!
c Done (mycputime is 2s).

Exit code

In order to automatically check the correctness of solver's answers, all solvers must also exit with an error code that must characterize its answer on the considered instance. This is done in addition to the automatic syntactic analysis of solver's output (results must be coherent, otherwise the answer is considered as BUGGY). We use conventions compatible with the ones used in Satex. The error code must be: Typically, if the solver is written in C,  a solver can end with such lines:
if (/* the formula has a model */) 
if (/* the model found gives the optimum value of the objective function */)
/* nobody can find a better solution */
fprintf(stdout, "s OPTIMUM FOUND\n");
outputCertificate(stdout); /* print an implicant */
/* we got a solution, but there may exist a better one */
fprintf(stdout, "s SATISFIABLE\n");
outputCertificate(stdout); /* print an implicant */
if (/* the formula has no model */)
/* definetely no way to find a model */
fprintf(stdout, "s UNSATISFIABLE\n");
/* er, too hard for me ! */
fprintf(stdout, "s UNKNOWN\n");

Buggy or not?

In the following cases a solver is considered buggy and will be returned to the author(s): For instance, if the solver crashes itself without giving any solution, it will not be strictly considered as "buggy" (even if this is due to some internal bug...), but its result will be considered as UNKNOWN.