Hot-path inefficiencies: full-scan BCP, no Clause equality, per-token regex compile

[paultristanwagner]

Severity: Medium · Category: performance · Confidence: high

Problem

• DPLLSolver.bcp iterates all clauses each round (naive O(C) scan watched literals exist to avoid).
• Clause has no equals/hashCode, so logically-identical learned clauses are duplicated in the DB and watch maps (unbounded growth during nextModel enumeration).
• Lexer.nextToken does Pattern.compile(regex) for every token type at every cursor position (O(tokens×types) recompiles on large DIMACS/CNF).
• CNF.parse is recursive on S -> (D) & S → StackOverflow on large inputs (relevant once DIMACS loading lands, #f17).

Location

sat/solver/DPLLSolver.java:96-122; sat/Clause.java; parse/Lexer.java:55; sat/CNF.java

Fix

Queue-based BCP; Clause.equals/hashCode + dedup on learn; precompile Patterns in TokenType; iterative CNF parse.