Arjun on Raspberry Pie about arjun HOT 4 CLOSED

Hi Axel,

Thank you so much for that uint64_t vs long unsigned bug. Good find, I have already fixed it in e5d37b6

The CNF indeed gets significantly smaller! Regarding getting back the solution, basically, we need to save from CryptoMiniSat:

• blockedClauses from occsimplifier.h
• variable replacement information from varreplacer.h called reverseTable
• interToOuterMain and varData from cnf.h

Then we need to feed that to Solutionextender along with the solution to the simplified CNF. This is basically what used to happen in the old system that extended a solution after pre-processing.

In arjun.cpp file in Arjun there is a function called get_fully_simplified_renumbered_cnf(). In that function there is a solver object. That solver (and not the solver object that's in arjun.h's struct Arjun) needs to call something like solver.save_state("toextend.dat") at the end of the function (just before return cnf;), to save the above 3 data pieces to file. This save_state() function does not exist. It's probably best to re-write it, although you can take hints from old CryptoMiniSat that had a saveState function that saved this (and more) information.

Once this data is saved, and the solution is found to the simplified CNF, we need to be able to extend the solution. For this, Arjun would need another function that loads the data of the 3 data pieces (blockedClauses, reverseTable and interToOuterMain) from "toextend.dat", takes the solution, and extends the solution, kinda how Solutionextender does it.

It's a little fiddly. However, if you can skip the BVA complexity (i.e. there are no BVA variables, so no XORs), then it's actually not that bad. Let me know if you wanna have a go at it!

from arjun.

OK, we now have preliminary support for this. You MUST re-build and reinstall CryptoMiniSat & Arjun. Then:

./arjun large.cnf simplified.cnf recovery
cadical simplified.cnf > solution
./solextend recovery solution > solution_final
./cnf-utils/verify_solution.py large.cnf solution_final

Where cadical is CaDiCaL from here: https://github.com/arminbiere/cadical but of course ANY sane SAT solver should work. And cnf-utils is: https://github.com/msoos/cnf-utils that provides solution verification.

The final solution is verified as correct. Note that there is likely an issue with so-called empty occurrence variables. These can be set to any value, but often NEED to be set to SOME value. These will likely make the system die. I'll work on that later.

For the moment, it seems to work, but has not been extensively tested. Handle with care. Will test later with a fuzzer.

from arjun.

BTW, this took 2 days and about 500 lines of total change, but should support our work on UniGen. I'm using Boost serialization library. Kinda cool, but it again had some weird compatibility issue with older gcc. So I had to work around that. Kinda painful. Otherwise it's kinda neat actually :)

from arjun.

Thank you!

I'm already feeling a bit guilty of time theft again.

from arjun.