[Cryptominisat-devel] Where to find removed variables ?

Mate Soos soos.mate at gmail.com
Lun 17 Jan 12:08:18 CET 2011


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

Hi Martin,

On 01/15/2011 01:38 PM, Martin Maurer wrote:
> 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 ?

I have just pushed a change into cluster129-fixed. If you do --dumpOrig,
it will now print into the CNF:

c -------------------------------
c previously eliminated variables
c -------------------------------
c ########### cls for eliminated var 2 ### start
- -726 163 2 -153 0
- -650 525 2 1113 0
- -525 117 2 322 1113 650 0
- -2 525 650 0
- -2 -525 -650 0
c ########### cls for eliminated var 2 ### finish
c ########### cls for eliminated var 10 ### start
626 1030 10 1078 65 0
199 -758 10 -1526 -357 0
- -626 -10 1030 1078 0
c ########### cls for eliminated var 10 ### finish

where the new things are those containing "####". You can clearly see
which var was eliminated, and that these vars appear in the clauses.
E.g. var 2 appears in the first 5 clauses as either "2" or "-2".

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/

iEYEARECAAYFAk00IyIACgkQsTOOstKb0jk6ygCgkKlxhjC38IR8rkdJ2Lrszrlh
k+oAn00Bi+QnVRwsTF4D5OuTOywy2AuH
=xUY+
-----END PGP SIGNATURE-----



More information about the Cryptominisat-devel mailing list