]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commit
Turning on simplification&subpart-solving in CMS2
authormsoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Wed, 28 Apr 2010 12:25:09 +0000 (12:25 +0000)
committermsoos <msoos@e59a4935-1847-0410-ae03-e826735625c1>
Wed, 28 Apr 2010 12:25:09 +0000 (12:25 +0000)
commitcba4184a3fdd68dc02a0f16c254f4cefbfc83ac1
treeae32c5dd18845312cf8bf38485225a51bd88de73
parent451d5bfea7fe53ee45da3cbc7e311570cd827d47
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