2015-10-14 [ap]
data/ru/4.0.batch CPU time (u+s seconds)
link-parser parameters: [-u] -panic -timeout=10000 data/ru/4.0.batch
Timing by: timeit -r 6 -n 6 "command>/dev/null" (best of multiple runs, rounded to 0.1)
The following statements in guiding.cpp are set differently, as indicated:
A solver->setDecisionVar(v, _parameters[v].isDecision);
B solver->varBumpActivity(v, _parameters[v].priority);
C solver->setPolarity(v, _parameters[v].polarity > 0.0);
(// means commented out.)
[*1]
A
B
C
[*2]
A
//B
//C
[*3]
A
// B
C
[*4]
// A
// B
// C
Standard parser: 16.7
sat-solver:
Current Minisat | Minisat-2.2+ | Glucose-4.0 | CryptoMiniSat(CMS)
------------------|---------------|--------------|----------------------
9.1 | 9.0 | 10.1 | 12.2
[*1] | [*2] | [*3] | [*4]
Note: The libraries that excels in very long English sentences Glucose-4.0 and CMS) are slower here.