]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commitdiff
Switch to multiplication variant 1.
authorFrancis Russell <francis@unchartedbackwaters.co.uk>
Tue, 19 Apr 2011 03:09:32 +0000 (04:09 +0100)
committerFrancis Russell <francis@unchartedbackwaters.co.uk>
Tue, 19 Apr 2011 03:09:32 +0000 (04:09 +0100)
CryptoMiniSat seems to work much better with multiplication variant one
(at least on my problems) so use it by default.

src/to-sat/BitBlaster.cpp

index f083cda22c6d2684422bdc9826ed6b097e3fdaae..67f1fe1b453042ee8b6ff78e5bfd04622c2428ca 100644 (file)
@@ -1572,7 +1572,8 @@ BBNodeVec BitBlaster<BBNode,BBNodeManagerT>::BBMult(const BBNodeVec& _x, const B
         y = _x;
       }
 
-         string mv = uf->get("multiplication_variant","3");
+      // Variant 1 seems to work best with CryptoMiniSat.
+      string mv = uf->get("multiplication_variant", "1");
 
       const int bitWidth = x.size();
       stack<BBNode> products[bitWidth];