Pseudo Boolean Evaluation 2005: requirements for solvers

Execution environment

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

  
	./mysolver instancefile.pb 12345

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

• PBTIMEOUT (the number of seconds it will be allowed to run),
• PBRAM (the amount of RAM in Mb available to the solver).
• PBSATISFIABILITYONLY (defined to 1 when the solver is only asked to answer if the formula is satisfiable or not, undefined otherwise)
  

/* To be used with "PBRAM" or "PBTIMEOUT or PBSATISFIABILITYONLY" */
/* 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 http://www.mpi-sb.mpg.de/units/ag2/software/opbdp/opbdp1.1.1.tar.gz). 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;

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

• A line starting with a '*' is a comment and can be ignored. Comment lines are allowed anywhere in the file.
• As a hint to perform memory allocation, the first line of the file will be a comment containing the word "#variable=" followed by a space and the number of variables in the file, then a space and the word "#constraint=" followed by a space and the number of constraints in the file. The space between the word and the number is mandatory to make parsing trivial. This information is only provided as a commodity for solvers which include a very limited parser. High quality provers are encouraged to ignore this information as it may not be accurate outside the evaluation environment (e.g. when a user creates a file by hand).
  
• Each non comment line must end with a semicolon ';'
• The first non comment line may be an objective function to minimize. It starts with the word "min:" followed by the linear function to minimize and terminated by a semicolon. No other objective function can be found after this first non comment line.
  
• A constraint is written on a single line and is terminated by a semicolon.
• An identifier represents the name of a boolean variable (atom).
• Each identifier must be followed by a space (so that it can be read by a function which reads a word from the file)
  
• The negation of an atom A will not appear in the file (it will be translated to 1-A)
  
• An integer may contain an arbitrary number of digits. There must be no space between the sign of an integer and its digits.

Benchmark files

Output Format

Messages

• comments (any information that authors want to emphasize, such as #backtracks, #flips,... or internal cpu-time), beginning with the two chars "c " (c and space)
• solution. Only one line of this type is allowed. This line must begin with the two chars "s " (s and space) and must be one of the following ones:
  • s SATISFIABLE
    this line must be output when the solver has found a solution but it can't prove that this solution give the least value of the objective function.
    
  • s OPTIMUM FOUND
    this line must be output when the solver has found a model and it can prove that no other solution will give a value of the objective function strictly less than the one obtained with this model. Let v be the value of the objective obtained with the valuation output by the solver.  Giving this result is a  commitment that  the formula extended with the constraint objective<v is unsatisfiable.
    
  • s UNSATISFIABLE
    this line must be output when the solver can prove that the formula has no solution.
    
  • s UNKNOWN
    this line must be output in any other case, i.e. when the solver is not able to tell anything about the formula
    
• values of a solution (if any), beginning with the two chars "v " (to be precised in the following).

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

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...
s SATISFIABLE
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!
s UNSATISFIABLE
c Done (mycputime is 2s).

Exit code

• 10 for SATISFIABLE
• 20 for UNSATISFIABLE
• 30 for OPTIMUM FOUND
  
• 0 for UNKNOWN
• any other error code for internal errors (considered as UNKNOWN)

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 */
    exit(30);
  }
  else
  {
    /* we got a solution, but there may exist a better one */
    fprintf(stdout, "s SATISFIABLE\n");
    outputCertificate(stdout);         /* print an implicant */
    exit(10);
  }
} 
else 
  if (/* the formula has no model */) 
  {
    /* definetely no way to find a model */
    fprintf(stdout, "s UNSATISFIABLE\n");
    exit(20);
  }
  else 
  {
    /* er, too hard for me ! */
    fprintf(stdout, "s UNKNOWN\n");
    exit(0);
  }

Buggy or not?

• It outputs UNSATISFIABLE for a satisfiable instance.
• It outputs SATISFIABLE, but provides an incorrect model (or an incorrectly formatted model).
• It outputs OPTIMUM FOUND but there exists a model with a better value of the objective function that the one obtained from the model found.
  
• The answer and the error code are not coherent.