Thanks, Peter. I think it's a very useful patch: it still allows us to use the more stable internal STP, as well as more recent versions of STP, including the svn one.
Best, Cristian On 09/07/10 16:24, Peter Collingbourne wrote: > Hi Daniel, > > Sorry for the slow response. > > On Thu, Apr 08, 2010 at 06:45:58PM -0700, Daniel Dunbar wrote: >> Um, ignore this question, since you obviously attached a patch for >> exactly this! :) >> >> It would be cool if we could tweak the patch to use the internal STP >> if --with-stp isn't specified, then we could go ahead and put it in >> trunk. > > I finally got round to doing this -- please see the attached patch. > I'll commit this if OK. > >>> It should be possible for us to support both options, >>> initially, which is nice for comparing the performance of them side by >>> side. Do you have any hard numbers that show that the new STP is >>> better, or by how much? > > On one particular benchmark, we experienced query runtimes of several > hours with the old STP, and approx 12 minutes with the new STP (dual > 2.0GHz machine, using CryptoMiniSat 2). I've attached a copy of the > problematic query. If you would like a copy of the benchmark itself > (it has a dependency on another library) I can try to do that. > > Thanks,
