// http://www.iiia.csic.es/~maxsat06/solver-requirements.html
// Format for the MaxSAT Competition 2006
// needs a semantic checker for:
// weight must be positve between 1 and 2^20
// variable name must be a positive integer between 1 and numVars 
// 
WCNF = Preamble Formula EOF.
Preamble = "p" "wcnf" <numVars> int <numClasues> int.
Formula = <clauses> List(Clause).
Clause = Weight <literals> List(Literal) ClauseTerminator.
Weight = <v> int.
ClauseTerminator = " 0".
List(S) ~ {S}.
Literal : Pos | Neg common Variable.
Variable : Numero | Name.
Numero = <v> int.
Name = <v> Ident.
Pos = .
Neg = "-".
Main = .