[Cryptominisat-devel] Shall dumporig cnf contain learnt binary clauses or not ?

Mate Soos soos.mate at gmail.com
Dim 2 Jan 14:26:27 CET 2011


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

Hi Martin,

On 12/30/2010 09:02 PM, Martin Maurer wrote:
> just testing a bit around / reading through sources with cluster 129 /
> master.
> 
> Following i wondered:
> 
> I started a cluster 129 version the following way:
> 
> cryptominisat64 --threads=6 --dumplearnts=10x10_learnt_50.cnf
> --maxdumplearnts=2 --dumporig=10x10_orig_50.cnf 10x10_orig_49.cnf
> 
> -> Displaying x variables and y clauses
> 
> After some time it found 8 new (binary) clauses.
> 
> Ok, i aborted. With cluster 129 version it created a dumporig cnf with
> name ...orig50.cnf
> 
> Now i restarted the same version with the generated file:
> 
> cryptominisat64 --threads=6 --dumplearnts=10x10_learnt_51.cnf
> --maxdumplearnts=2 --dumporig=10x10_orig_51.cnf 10x10_orig_50.cnf
> 
> I see that it started with x variables and y clauses. Where are my 8
> learnt clauses ?
> 
> Ok, aborted, new trial with previous dump orig cnf (but additional
> --alsoread=10x10_learnt_50.cnf)
> 
> cryptominisat64 --alsoread=10x10_learnt_50.cnf --threads=6
> --dumplearnts=10x10_learnt_51.cnf --maxdumplearnts=2
> --dumporig=10x10_orig_51.cnf 10x10_orig_50.cnf
> 
> And indeed, now it displays y + 8 clauses during start.

This is the correct behaviour.

When dumping the original problem, we don't dump learnt clauses. The
learnt clauses, also called "redundant" clauses don't form part of the
original (also called "irredundant") clause set. The good thing about
"dumporig" is that if the original clauses have been shortened, removed,
or variables have been set and/or replaced, that will be reflected in
the dumped CNF. We don't want to add learnt binary clauses to this
dumped problem, as it has been standard by every SAT researcher that
learnt and non-learnt clauses have been separately treated.

By the way, I am starting to break this unofficial rule in the master
branch for a number of reasons, but I am only doing learnt to non-learnt
conversion in certain circumstances (only binary, etc.). Note that it is
always safe to make a learnt clause into non-learnt, but not vica-versa,
as learnt clauses can be cleaned (=removed) at any moment.

The conclusion is to do:

./cryptominisat --dumporig=prob_cleaned.cnf
- --dumplearnts=prob_learnt.cnf --maxdumplearnts=3 --restarts=20 problem.cnf

and then:

./cryptominisat --alsoread=prob_learnt.cnf prob_cleaned.cnf

Though nowadays lots of state is saved in prob_learnt.cnf, so you might
try to remove "--maxdumplearnts" altogether.

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/

iEYEARECAAYFAk0gfQMACgkQsTOOstKb0jmK8ACggYISM4gisckCjxIhAlFdfYw3
vFwAn3MDqCEGg5GV9uWOHEoUiyhzt/3/
=SXAh
-----END PGP SIGNATURE-----



More information about the Cryptominisat-devel mailing list