From cd711089d72adb027b93b0860ba45387c239807e Mon Sep 17 00:00:00 2001 From: Mahesh Madhav Date: Tue, 3 Sep 2024 04:30:14 +0000 Subject: [PATCH 1/2] Perf improvement in satsolver Switch one FP divide to an FP multiply (variable is constant). Calculate ratio inside of verbosity clause, since that is where it is used. --- src/sat/bsat/satSolver.c | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index eea280293..ebb6fcce1 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -62,7 +62,8 @@ static inline double drand(double* seed) { *seed *= 1389796; q = (int)(*seed / 2147483647); *seed -= (double)q * 2147483647; - return *seed / 2147483647; } + return *seed * 4.6566128752457969e-10; // 1.0/2147483647.0 +} // Returns a random integer 0 <= x < size. Seed must never be 0. @@ -1954,12 +1955,12 @@ int sat_solver_solve_internal(sat_solver* s) while (status == l_Undef){ ABC_INT64_T nof_conflicts; - double Ratio = (s->stats.learnts == 0)? 0.0 : - s->stats.learnts_literals / (double)s->stats.learnts; if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit ) break; if (s->verbosity >= 1) { + double Ratio = (s->stats.learnts == 0)? 0.0 : + s->stats.learnts_literals / (double)s->stats.learnts; printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", (double)s->stats.conflicts, (double)s->stats.clauses, From ad8f8a2aabb7531df5a8ec6091494da2462a4f6a Mon Sep 17 00:00:00 2001 From: Mahesh Madhav Date: Tue, 3 Sep 2024 04:48:07 +0000 Subject: [PATCH 2/2] Convert the other divide to a multiply --- src/sat/bsat/satSolver.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index ebb6fcce1..6b246a2e6 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -60,7 +60,7 @@ static void printlits(lit* begin, lit* end) static inline double drand(double* seed) { int q; *seed *= 1389796; - q = (int)(*seed / 2147483647); + q = (int)(*seed * 4.6566128752457969e-10); // 1.0/2147483647.0; *seed -= (double)q * 2147483647; return *seed * 4.6566128752457969e-10; // 1.0/2147483647.0 }