Arjun on Raspberry Pie

[a1880]

Hi Mate,

First I tried to port Arjun to Windows. I couldn't get around the problem that "find_equiv_subformula()" is no known method of CMSat::SATSolver. Something must have confused my compiler (MS VC++ 2022). (update 03-Mar-2023: Turned out to be my fault: I used cms 5.11.2 rather than 5.11.4) For the time being, I gave up the porting and resorted to my Raspberry Pie.

Building and testing Arjun on a Raspberry Pie went smoothly overall. However, I’ve encountered the following issues: (I hope that you don't mind to get this "bundle" of issues rather than several separate issues)

To circumvent a compile error (known from my Windows port), I had to change the following return type in Arjun.h (line 145)

       //  long unsigned get_backbone_simpl_max_confl() const;
       uint64_t get_backbone_simpl_max_confl() const;

As found by @ale-depi, I had to execute the following before running arjun

sudo ldconfig -v

Otherwise, the shared libaries like liblouvain_communities.so.1.0 are not found.

During make, I got a lot of warnings. I hope and assume that these can be ignored.

For a CNF example with interspersed xcnf/XOR clauses, I got an assertion failure:

arjun: /home/ak/cppsrc/arjun/src/arjun.cpp:103: bool ArjunNS::Arjun::add_xor_clause(const std::vector<unsigned int>&, bool):
Assertion `false && "Funnily enough this does NOT work. The XORs would generate a BVA variable, and that would then not be
returned as part of the simplified CNF. We could calculate a smaller independent set, but that's all."' failed.

I would be interested to contribute a mapping tool to get the original literal IDs back. Do you have any hints, where I could start/look to get this accomplished?

I tried two examples and got a massive reduction in variables and clauses. 964 variables in 3088 clauses shrunk to 452 variables in 2704 clauses 3248 variables in 10808 clauses where simplified to 1520 variables in 9594 clauses.

Now I am curious, if the resulting SAT solution is correct and easy/easier to find.

Greetings,

Axel

[msoos]

Hi Axel,

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

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!

[msoos]

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.

[msoos]

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 :)

[a1880]

Thank you!

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