CliqueSolver
Finding cliques in graphs using SAT
-
- Background
-
-
The Clique Problem is in NP.
-
Therefore, it is poly-time reducible to SAT.
-
I found such a reduction on the internet.
-
This program implements that reduction.
-
This small tool uses the .dot language. Dot files are viewable graphically here.
-
- Usage
-
-
Input: a .dot file describing an undirected graph (for now, the vertices must be numbers) and a number k - the size of the desired clique.
-
Output: If there is a clique of size k, the output is a dot file with the clique marked in red.
-
Execution:
-
Download the jar file.
-
Go to the directory of the downloaded jar file.
-
Run "java -jar cliquesolver.jar find ".
-
- Example
-
-
- Downloads
-
-
- Remarks
-
-
I've used the jgrapht library for representing graphs.
-
I've used sat4j for SAT solving.
-
There is an additional feature in this program. If you run "java -jar cliquesolver.jar analysis k", the program will generate an excel file, comparing the running time results of the reduction, using all solvers of sat4j. In addition, it will compare all of them to a clique-finding algorithm implemented in jgrapht, that has no connection to the reduction. The calculations will be made on random graphs with maximum k vertices. After playing with the analysis feature, one can easily see that using the reduction (at least as I have) isn't a very good heuristic for searching for cliques of size that is proportional to the number of vertices. However, the implementation is still a fun experiment.