From cba4184a3fdd68dc02a0f16c254f4cefbfc83ac1 Mon Sep 17 00:00:00 2001 From: msoos Date: Wed, 28 Apr 2010 12:25:09 +0000 Subject: [PATCH] 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 --- src/to-sat/ToSAT.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/to-sat/ToSAT.cpp b/src/to-sat/ToSAT.cpp index 555660e..dc7952d 100644 --- 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 && -- 2.47.3