# Parser for CNF formulas

I have a parser for CNF formulas in Dimacs format, which is very slow. Any suggestion on how to improve its speed? I did some profiling and I might have to replace Scanner. Is there anything faster?

A possible input for the parser is:

c A sample .cnf file.
p cnf 3 2
1 -3 0
2 3 -1 0


The code:

/**
* Parses a stream for a CNF instance.
*
* @param source input stream
* @throws ParseException if stream contains an invalid instance
*/
private static Skeleton parseStream(final InputStream source)
throws IOException, ParseException {
Scanner scanner = new Scanner(source);

try {
String token = scanner.next();
while (token.equals("c")) {
scanner.nextLine();
token = scanner.next();
}
if (!token.equals("p")) {
throw new ParseException(
"Excepted 'p', but '" + token + "' was found");
}
} catch (NoSuchElementException e) {
}

int numVariables, numClauses;
try {
String cnf = scanner.next();
if (!cnf.equals("cnf")) {
throw new ParseException(
"Expected 'cnf', but '" + cnf + "' was found");
}
numVariables = scanner.nextInt();
numClauses = scanner.nextInt();
} catch (NoSuchElementException e) {
}
logger.debug("p cnf " + numVariables + " " + numClauses);

Skeleton skeleton = new Skeleton(numVariables);
try {
while (numClauses > 0) {
int literal = scanner.nextInt();
if (literal == 0) {
numClauses--;
}
}
} catch (NoSuchElementException e) {
throw new ParseException(
"Incomplete problem: " + numClauses + " clauses are missing");
}

return skeleton;
}

• I suggest you to use ANTLR to generate parsers. It also provides you with some useful operations. You can find all you need. When you don't want to just learn how to write a parser from scratch then you should not reinvent the wheel. Apr 8 '11 at 7:51
• Are you sure it's the parsing that is the bottleneck here? Simply reading data from disk is an expensive operation, so, it could be just that.
– user3008
Apr 8 '11 at 19:26

Use a BufferedInputStream to speed up the disk access. If that's not enough, you can read the file line-by-line and use split() to break it into individual numbers.