[Cryptominisat-devel] more good news, plus question

Mate Soos soos.mate at gmail.com
Sam 22 Jan 11:16:53 CET 2011


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

Hi Robert,

On 01/20/2011 10:07 PM, Robert Aston wrote:
>    I have downloaded the latest pre-release 2.9.0, compiled it and run
> it on all the test cases I have, (large and small).  All are working.

Good news, thank you!

> I'm now back to developing my Sudoku solver.  Using Cryptominisat, I can
> solve any puzzle within a second.

Really any puzzle? Because The larger these get, the more difficult they
are, in an exponential way, I think... so for really large puzzles I
thought that you would hit a wall :O

> My question is this.  Is there an option
> within Cryptominisat that I can invoke that will same to a file, (or
> display on the screen), the order in which each variable is solved?
> Knowing this, I can work out the Sudoku solution order.

Well, we could do that ;) Essentially, you wish to have an output like
this, right?:

c ------------------------------
c search tree of found solution:
c
c (1) branched on Lit  5. Propagated lits:  5 -10  -4
c (2) branched on Lit -2. Propagated lits: -7   1  -3
c (3) branched on Lit  8. Propagated lits: -9   6
c (4) All variables set: solution found.
s SATISFIABLE
v 1 -2 -3 4 5 6 -7 8 -9 -10

I can do this very quickly.

Bests,

Mate

-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.10 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAk06rpUACgkQsTOOstKb0jkBOQCfZJkn7NK1b1Sm1Myl7N64w0E7
ZYcAn1aHrKZgrmWG6uvYGy1raJuPSxs1
=AYLj
-----END PGP SIGNATURE-----



More information about the Cryptominisat-devel mailing list