Regarding the competition buiild of the Iroots algorithm

[Jeremias Berg]

Hello
My name is Jeremias Berg and I work at Helsinki university.
We're studying how to map clustering problems into partial MAX-SAT and
using a variety of solvers for testing the encoding.
I've been experimenting a bit with the competition, (Max SAT evaluations
2012) build of ubcsat-irots, however I'm a bit confused on how to
use the solver for solving partial problems.

Right now I encode my hard clauses to have a weight higher than all of
the soft clauses combined, and start the file with:
p wcnf NUMBER_VARIABLES NUMBER_CLAUSES TOP_WEIGHT. My files have an
ending of ".wcnf"

However I stil ran into some instances where the solution, and
specifically the second set of solutions (the output seemed to have two
assignments for some of the solvers) to be printed out by the solver,
broke some of the hard clauses. Is there something I'm missing?


--
Jeremias Berg

[Dave Tompkins]

Hi Jeremias...

Because of the way that local search (incomplete) algorithms work, they essentially ignore the TOP_WEIGHT argument.

Note that the competition build is really specialized for the competition:

* it stops after ~300 (295) seconds, and prints a solution at 240 seconds too (hence the confusing double output)

You should really use the regular build of ubcsat.  The version with maxsat in it is 1.2-b17:

https://github.com/dtompkins/ubcsat/tree/beta

the hard-coded arguments for the competition were:

ubcsat -alg irots -w -i FILENAME -q -r maxsatcomp stdout 240 -cutoff max -abstime -systime -gtimeout 295 

depending on what you're looking for I can recommend some parameter settings (ubcsat has a lot)

if you know what your target (optimal) solution quality [sum of unsatisfied clauses] is, you can specify it with -wtarget INT.

This will run forever until it finds that target:

ubcsat -alg irots -w -i FILENAME -cutoff max -wtarget INT

so if (for example) you want to make sure just your hard constraints are met, you could set that as your target.

you should add [-r maxsatcomp FILENAME INT] to generate the same competition report, outputing every INT seconds the best solution known so far.

just run ubcsat (no parameters) to get some basic help

Feel free to let me know if you need more help.

-Dave