From d7a3d82429cedc668f500ed2e7e8145a894f88fc Mon Sep 17 00:00:00 2001 From: Francis Russell Date: Tue, 19 Apr 2011 04:09:32 +0100 Subject: [PATCH] Switch to multiplication variant 1. 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 | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/to-sat/BitBlaster.cpp b/src/to-sat/BitBlaster.cpp index f083cda..67f1fe1 100644 --- a/src/to-sat/BitBlaster.cpp +++ b/src/to-sat/BitBlaster.cpp @@ -1572,7 +1572,8 @@ BBNodeVec BitBlaster::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 products[bitWidth]; -- 2.47.3