[Cryptominisat-devel] Where to find removed variables ?

Mate Soos soos.mate at gmail.com
Sam 15 Jan 13:18:04 CET 2011


-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Dear Martin,

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 (100 
> variables less).
> 
> Perhaps two hints, where i see the number "100":
> 
> c Removed useless bin:       0  fixed:     0  props:  20.00M  time:  0.45 s
> c lits-rem:         0  cl-subs:        0  v-elim:    100  v-fix:    0  time: 
> 3.74 s
> 
> and
> 
> 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,

Bests,

Mate


- -- 
Mate Soos
Security Research Labs
http://www.srlabs.de
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAk0xkHsACgkQsTOOstKb0jnTJwCbB0ZOcQUvzH/EGp3waawkN941
YA4An01qmhxc73flZ0tlvtToTl0ZilOh
=e3v3
-----END PGP SIGNATURE-----



More information about the Cryptominisat-devel mailing list