UBCSAT: Flipping Multiple Variables

[Andrew Edwards]

Dear Dave, and the UBCSAT team,

I am a senior undergraduate CMPS student at UCSC. I am currently lucky enough to be working with Dimitris Achlioptas on my senior thesis, and the main focus of my study has been satisfiability and combinatorial optimization.

I have used the UBCSAT framework to test the performance of multiple SLS algorithms. Late last year I implemented a version of Adrian Balint’s ProbSAT. I want to personally thank you for the software framework; development is easy and the performance is very good.

I am interested in testing algorithms that flip multiple variables per step. Is there a good way to implement this? I understand that this could be achieved by breaking up the flips into multiple steps, but it would be very nice to be able to specify an assignment for a clause in a single step. I read on the Google group that you implemented an algorithm akin to Moser’s LLL-random walk algorithm, but I cannot find it on Github (I looked for the tag v1.2beta13 but found nothing).

If there is still no good way to do this, I would be interested in helping implement the feature. I would also appreciate seeing your implementation of the “lllwalk”.

Thank you,
Andrew Edwards

[Dave Tompkins]

Hi Andrew.

The code is in the "beta" branch in github:

https://github.com/dtompkins/ubcsat/blob/beta/src/random.c

you can see the code at the bottom for the LLLWalk algorithm.

It only does one (possible) flip per step, using a counter iLLLWalkClausePosition to keep track of which var in the clause to potentially flip... when that's zero, it selects a new unsat clause.

Introducing the multiple flips per "step" may break other components (caching which clauses are currently unsat, etc.)

For convenience, I would recommend you do something similar to what LLLWalk does for your project.  You could determine all at once which vars to flip and store them in an array, but then just spread those flips out over several steps.

What we could do is add a new "real step" statistic [or something like that] so you could collect the data and distinguish between "flips" and "steps" in your stats.

let me know if you need any additional help.

-Dave