graph coloring with a SAT solver

[Tom Sirgedas]

- Some SAT solvers: http://www.satcompetition.org/2009/format-benchmarks2009.html

- Input is a DIMACS file

  - which is a boolean expression in CNF form: https://en.wikipedia.org/wiki/Conjunctive_normal_form

  - example boolean expression: "(A or ~B) and (~A or B)" where A and B are true/false variables (though DIMACS uses numbers for the variables)

- Output is

  - "UNSATISFIABLE" if there's no true/false assignment to the variables to make the expression true

  - "A=false, B=false" if these assignments make the expression true (the actual output is "-1 -2", meaning variables 1 and 2 are both false)

Once you're comfortable with that, you can color graphs:

https://cs.stackexchange.com/questions/42397/how-do-you-produce-a-cnf-from-a-circular-graph-with-colouring

[jaan3...@gmail.com]

Thank you, Tom.

Are some solvers available under Windows?

[Tom Sirgedas]

I'm on Windows and it was a struggle to find anything. Aubrey mentioned Mathematica has a SAT solver, so that's one option.

I got glucose to run on my home machine, but it was a big pain. I installed Cygwin, which emulates Linux on Windows, installing C++  and some other packages (can't remember the exact steps), and got the glucose source code and compiled it, and only got the "simp" version of it to work. I can try to reproduce the steps if you're up for the challenge.

I got Cadical to work well enough. I got it to compile with Visual Studio, but it needed some modifications. It worked, but it struggled with problems that glucose solved. (Typically problems are either solved nearly instantaneously or take "forever"). I could share an EXE for Cadical, or the modified source, if that interests you.

Maybe I'll try porting glucose to Windows again, though I got stuck last time.

[mr.t...@gmail.com]

In case you find it easier to use, CryptoMiniSAT works on Windows and you should be able to build it unchanged with Visual Studio (if not, make an issue on the GitHub - Mate is very good about fixing bugs). It's pretty competitive with other state-of-the-art solvers.

On the other hand, I'm not sure if generic SAT solvers are really the best way to do graph coloring - it's often the case that you can greatly improve solver performance on particular classes of instances by tuning its parameters. People must have investigated specialized solvers for graph coloring (there's lots you could do, e.g. symmetry breaking), but I haven't looked myself.

[Tom Sirgedas]

Nice!

I did get the "simp" version of Glucose to compile on Windows, so I'll try to clean that up and provide binaries. Maybe I'll do the same for CryptoMiniSAT.

[Tom Sirgedas]

I made this github repo for a Windows port of Glucose: https://github.com/TomSirgedas/glucose-syrup-4.1-Windows
Here's a zip of the x86/x64 executables: glucose-syrup-4.1-Windows-binaries.zip (browser may warn that it's not downloaded much)

[Tom Sirgedas]

re: symmetry breaking, I recently realized that if you try to 7-color a graph, the simple translation to SAT will allow 7! permutations of colors to all be valid solutions. You pick an arbitrary vertex and force it to be color 0, which speeds up the search (potentially 7-fold) without losing anything. Now, I'm finding the largest clique I can and assigning each element a specific unique color. (An additional small improvemet: I'm also picking an arbitrary vertex outside the clique and forcing it to either match a color in the clique, or a 1 specific other color -- I think it would help most if the arbitrary vertex has many edges to the clique). This optimization helps GREATLY for UNSAT problems, since MANY symmetric permutations aren't considered.

[Tom Sirgedas]

Does anyone have recommendations for a weighted MAX-SAT solver?

[mr.t...@gmail.com]

I've used MaxHS, one of the best solvers, although it needs CPLEX (which you may be able to get for free through IBM's Academic Initiative). However it was finally dethroned in this year's competition by RC2, which I haven't tried myself but is part of PySAT and so should be easy to use (although the repo says it hasn't been tested on Windows).

[Tom Sirgedas]

Thanks Mr.Theta!! I was able to get MaxHS working on Windows. I'm not a student, but I was still able to get CPLEX:

Using IBM CPLEX version 12.8.0.0 under IBM's Academic Initiative licencing program

It mentioned a restriction of 1000 variables or clauses or something, but I haven't run into that yet. 

[Tom Sirgedas]

Update: I hit the limit

 

c WARNING. CPLEX Failed to optmize MIP
c WARNING. CPLEX Error  1016: Promotional version. Problem size limits exceeded.
c WARNING. Cplex status = 0
c ERROR: Cplex::solve() failed
c unsolved

[jaan3...@gmail.com]

Tom, thank you very much, especially for executables of Glucose. I started from SAT-solver, integrated into Mathematica (and based on MiniSAT libraries, as I understand). Now I've got many questions about SAT possibilities in application to graph coloring problem. It is interesting to compare timings of various solvers. The main question is how large could be the graph (10^5, 10^6 vertices) to be checked successfully? Thanks to you I can run Glucose. I've tried some graphs. Mathematica solver seems to be 2 times slower at this momemt, but more interesting is to try Glucose for large graphs, where Mathematica fails (on my computer, which might be slow too). 

You said about symmetry breaking, that it is useful for UNSAT. Is it right, that this does not help with SAT solution? What tricks could be used for SAT? 

What additional features has CryptoMiniSAT (in addition to parallelism and many options)? Could it be more powerful for graph coloring?

[Tom Sirgedas]

Hey, I updated the glucose binaries so that the "certificate" options is available.

Also, piping in input from "stdin" is now possible.