From de78f96c41606556b154dc4f220e00c3de6340e1 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Fri, 4 Dec 2009 00:09:09 +0000 Subject: [PATCH] played with cryptominisat parameters to improve performance git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@451 e59a4935-1847-0410-ae03-e826735625c1 --- src/sat/cryptominisat/Solver.cpp | 4 ++-- src/to-sat/CallSAT.cpp | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/cryptominisat/Solver.cpp b/src/sat/cryptominisat/Solver.cpp index 01a4d8a..3722015 100644 --- a/src/sat/cryptominisat/Solver.cpp +++ b/src/sat/cryptominisat/Solver.cpp @@ -35,8 +35,8 @@ namespace MINISAT Solver::Solver() : // Parameters: (formerly in 'SearchParams') - var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02) - , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1) + var_decay(1 / 0.99), clause_decay(1 / 0.999), random_var_freq(0.02) + , restart_first(100), restart_inc(1.0), learntsize_factor((double)1/(double)3), learntsize_inc(1.1) // More parameters: // diff --git a/src/to-sat/CallSAT.cpp b/src/to-sat/CallSAT.cpp index a3e7317..bf2fdcc 100644 --- a/src/to-sat/CallSAT.cpp +++ b/src/to-sat/CallSAT.cpp @@ -8,7 +8,7 @@ ********************************************************************/ #include "ToSAT.h" -#define MAX_BUCKET_LIMIT 3 +#define MAX_BUCKET_LIMIT 4 namespace BEEV { -- 2.47.3