7
\$\begingroup\$

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                                                                           
 * @return read skeleton
 * @throws ParseException if stream contains an invalid instance                                        
 */
private static Skeleton parseStream(final InputStream source)                                           
    throws IOException, ParseException {                                                                
  Scanner scanner = new Scanner(source);                                                                

  // Skip comments
  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) {
    throw new ParseException("Header not found");                                                       
  }

  // Reads header
  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) {
    throw new ParseException("Incomplete header");                                                      
  }
  logger.debug("p cnf " + numVariables + " " + numClauses);                                             

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

  return skeleton;                                                                                      
}                                                                                                       
\$\endgroup\$
  • \$\begingroup\$ 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. \$\endgroup\$ – Amirh Apr 8 '11 at 7:51
  • \$\begingroup\$ 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. \$\endgroup\$ – user3008 Apr 8 '11 at 19:26
7
\$\begingroup\$

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.

| improve this answer | |
\$\endgroup\$
  • \$\begingroup\$ Same exact suggestion I was going to give \$\endgroup\$ – Joe Phillips Feb 16 '11 at 21:20

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.