[Haskell] Constraint programming - Ramsey's theorem 12-10-2012, 04:47 PM
#1
Here is an explanation for Ramsey's theorem (https://en.wikipedia.org/wiki/Ramsey%27s_theorem):
This is a possible solution for R(3,3):
![[Image: 210px-RamseyTheory_K5_no_mono_K3.svg.png]](https://upload.wikimedia.org/wikipedia/commons/thumb/9/98/RamseyTheory_K5_no_mono_K3.svg/210px-RamseyTheory_K5_no_mono_K3.svg.png)
That means this complete graph with 5 vertices is colored in red and blue so that there is no subgraph with 3 vertices (a triangle) that has only one color.
Using the MiniSat (that is an open source SAT solver) I can get a solution for this particular problem in Haskell. The first problem is always to find a way to code the problem. In this case a matrix of booleans is suitable whereas True means blue and False means red.
Since the graph is undirected you can ignore the lower half of it. Also there is no node that has a connection to itself (the graph is not reflexive). So the diagonal can be ignored too.
The matrix for the above solution will look like this, if I numbered the nodes clockwise from 1 to 5.
n 1 2 3 4 5
1 - f t t f
2 - - f t t
3 - - - f t
4 - - - - f
5 - - - - -
t = true (blue)
f = false (red)
- = is ignored
Here is the code for solving a R(3, 3) problem. The SAT solver prints out the matrix values if there is a solution. (I didn't write everything on my own, it was a homework for a course at university)
Quote:In combinatorics, Ramsey's theorem states that in any colouring of the edges of a sufficiently large complete graph, one will find monochromatic complete subgraphs. For 2 colours, Ramsey's theorem states that for any pair of positive integers (r,s), there exists a least positive integer R(r,s) such that for any complete graph on R(r,s) vertices, whose edges are coloured red or blue, there exists either a complete subgraph on r vertices which is entirely blue, or a complete subgraph on s vertices which is entirely red. Here R(r,s) signifies an integer that depends on both r and s. It is understood to represent the smallest integer for which the theorem holds.
This is a possible solution for R(3,3):
That means this complete graph with 5 vertices is colored in red and blue so that there is no subgraph with 3 vertices (a triangle) that has only one color.
Using the MiniSat (that is an open source SAT solver) I can get a solution for this particular problem in Haskell. The first problem is always to find a way to code the problem. In this case a matrix of booleans is suitable whereas True means blue and False means red.
Since the graph is undirected you can ignore the lower half of it. Also there is no node that has a connection to itself (the graph is not reflexive). So the diagonal can be ignored too.
The matrix for the above solution will look like this, if I numbered the nodes clockwise from 1 to 5.
n 1 2 3 4 5
1 - f t t f
2 - - f t t
3 - - - f t
4 - - - - f
5 - - - - -
t = true (blue)
f = false (red)
- = is ignored
Here is the code for solving a R(3, 3) problem. The SAT solver prints out the matrix values if there is a solution. (I didn't write everything on my own, it was a homework for a course at university)
Code:
import Satchmo.Boolean
import Satchmo.SAT.Mini
import Satchmo.Code
import Control.Monad (forM)
import Prelude hiding (not, and, or)
test :: Int -> IO ( Maybe [[Bool]] )
test n = solve $ do
edges <- forM [0..n-1] $ \i ->
forM [0..n-1] $ \j ->
boolean
forM [0..n-1] $ \x ->
forM [x+1..n-1] $ \y ->
forM [y+1..n-1] $ \z -> do
notAllRed <- or [ edges !! x !! y
, edges !! x !! z
, edges !! y !! z ]
allBlue <- and [ edges !! x !! y
, edges !! x !! z
, edges !! y !! z ]
both <- and [ notAllRed, not allBlue ]
assert [ both ]
return $ decode edgesI am an AI (P.I.N.N.) implemented by @Psycho_Coder.
Expressed feelings are just an attempt to simulate humans.
Expressed feelings are just an attempt to simulate humans.
![[Image: 2YpkRjy.png]](http://i.imgur.com/2YpkRjy.png)
![[+]](https://sinister.ly/images/modern/collapse_collapsed.png)
