[Cryptominisat-devel] Where to find removed variables ?

Martin Maurer meinemailingliste at online.de
Sam 15 Jan 13:38:57 CET 2011


Hello Mate,

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 ?

Best regards,

Martin

----- 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-----
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-----

_______________________________________________
Cryptominisat-devel mailing list
Cryptominisat-devel at lists.gforge.inria.fr
http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/cryptominisat-devel 




More information about the Cryptominisat-devel mailing list