PB06: Input Format
This is an archived description of the PB06 input format. For the
PB07 evaluation, this format is maintained for linear pseudo-Boolean
instances.
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= 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 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> <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:
- 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.
- A boolean variable (atom) is named by a lowercase 'x' followed by
a strictly positive integer number. The integer number can be
considered as a
identifier of the variable. This integer identifier is strictly less
than 232. Therefore, a solver can input a variable name by
reading a character (to skip the 'x') and then an unsigned long
int.
- Inside the evaluation environment, variable names are guaranteed
to range from "x1" to "xN" where N is the total number of variables in
the instance (as given on the first line of the file). Each variable
between x1 and xN will occur in at least one constraint or the
objective function. High quality provers are
encouraged to avoid relying on this assumption as it may not hold
outside
the evaluation environment.
- Inside the evaluation environment, each
variable present in the objective function will occur in at least one
constraint. High quality provers are
encouraged to avoid relying on this assumption as it may not hold
outside
the evaluation environment.
- Each variable name must be followed by a space
- The negation of an atom A will not appear in the file (it will be
translated to 1-A)
- The weight of a variable may contain an arbitrary number of
digits. There must
be no space between the sign of an integer and its digits.
- Lines may be very long. Programmers should avoid reading a line
as a whole.
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.