[Cryptominisat-devel] Where to find removed variables ?
meinemailingliste at online.de
Sam 15 Jan 13:38:57 CET 2011
can i find out which variable was eliminated ? E.g. can i put a debug output
somewhere in source (just for testing)
to print out which variable was removed ?
----- Original Message -----
From: "Mate Soos" <soos.mate at gmail.com>
To: <cryptominisat-devel at lists.gforge.inria.fr>
Sent: Saturday, January 15, 2011 1:18 PM
Subject: Re: [Cryptominisat-devel] Where to find removed variables ?
-----BEGIN PGP SIGNED MESSAGE-----
On 01/15/2011 11:51 AM, Martin Maurer wrote:
> I call it the following, but abort it after some short time:
> As you can see the number of variables was reduced from 17056 to 16956
> variables less).
> Perhaps two hints, where i see the number "100":
> c Removed useless bin: 0 fixed: 0 props: 20.00M time: 0.45
> c lits-rem: 0 cl-subs: 0 v-elim: 100 v-fix: 0
> 3.74 s
> c v-elim SatELite : 100 (0.59 % vars)
> I am happy to find 100 variables (their value), but where can i find which
> variables were set to which value ?
Unfortunately, this only means that the variables were eliminated. In
other words, every occurance of the variable was eliminated ("v-elim")
using the resolution rule, which states:
a V -c
a V d
- -a V g
- -a V -h
- -c V g
- -c V -h
d V g
d V -h
Which typically produces more clauses than the original (in above case,
it's 2x2 = 2+2, so this is an exception). Unfortunately, we don't find
the values for these variables.
I hope I have helped,
Security Research Labs
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
-----END PGP SIGNATURE-----
Cryptominisat-devel mailing list
Cryptominisat-devel at lists.gforge.inria.fr
More information about the Cryptominisat-devel