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


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

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,



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


Cryptominisat-devel mailing list
Cryptominisat-devel at lists.gforge.inria.fr

More information about the Cryptominisat-devel mailing list