Turning on simplification&subpart-solving in CMS2

Simplification is carried if the problem seems difficult. It is carried
out in steps, so the complete algorithm's time demands do not have to
absorbed the first time it is run. Subpart-solving regularly checks for
parts of the problem that are disconnected, solves them, and returns to
the original problem instance -- essentially executing a
divide-and-conquer algorithm

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@732 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp
index 555660ebf2f8b830a3e9f58615ccc6ae1dbb54c9..dc7952decf115494769612f61247bd49e834054c 100644 (file)
--- a/src/to-sat/ToSAT.cpp
+++ b/src/to-sat/ToSAT.cpp
@@ -135,9 +135,10 @@ namespace BEEV
 
 #if defined CRYPTOMINISAT2
     newSolver.findNormalXors = false;
-    newSolver.doSubsumption = false;
+    newSolver.doSubsumption = true;
     newSolver.verbosity = 0;
-    newSolver.doPartHandler = false;
+    //newSolver.fixRestartType = static_restart;
+    newSolver.doPartHandler = true;
 #endif
 
 //     if(enable_clausal_abstraction &&