Syntax of Minweight Instances
-
Variables
-
Variables are represented by positive integers.
The first variable is variable 1.
-
Literals
-
Literals are represented as a both positive and
negative integers, with the obvious meaning.
-
Clauses
-
Each clause is represented by a single line composed
of its literals (separated by spaces), ending with 0
-
Formula
-
The formula is a set of clauses, and is therefore
represented as a sequence of lines. A formula may
end with a line containing only :, or
%. In the second case, all weights are
assumed to be 0.
-
Weights
-
After the : character, there is a sequence of
lines, each containing a single nonnegative integer,
representing the weight of a variable. The first line
is the weight of the first variabile, and so on. If
there are more variabiles than weight lines, the remaining
variabile are assumed to weight 0. The set of weight
is ended by the character %.
Example: the set of clauses
{ x1 v -x2,
x2 v x3 v x4 }, where variabiles
x1 and x3 are weighted 1,
while the other ones are weighted 0, can be represented by:
1 -2 0
2 3 4 0
:
1
0
1
%
Lines starting with 'c' or 'p' are ignored.