From: Patrick Prosser
Sent: 12 October 2010 15:23
To: Chris Beck
Cc: Patrick Prosser
Subject: Modeling independent set in CP, SAT, and SCIP
Just a brief note on modelling independent set in CP, SAT, and in SCIP, and
why this is interesting.
First, it would be nice to have a simple encoding for independent set (indSet)
that can be solved with CP and SCIP without modification. That way we can
directly compare CP and SCIP and determine if phase transition behaviour in CP
is same as that in SCIP. A second CP/SAT-only model would also be nice,
hopefully to demonstrate that phase transition behaviour in CP is model-
independent and that SAT solver has same behaviour as CP. So, first a CP and
SAT model, second a SCIP and CP model
CP Model for indSet
--------------------
This is trivial. For a graph G = (V,E) we have a 0/1 decision variable v[i]
for each vertex in G. For each edge (i,j) in E we have the constraint v[i] +
v[j] < 2. We maximise the sum of the variables v[1] + ... + v[n]. This model
could be solved with any CP toolkit and also minisat+.
SCIP & CP model for indSet
--------------------------
Given a square array A[n][n] of 0/1 constants where A[i][j] = 1 iff vertex i
is adjacent to vertex j. In addition A[i][i] = n, the number of vertices in
the graph. A vector of 0/1 decision variables v[1] to v[n] where v[i] = 1 iff
vertex i is selected. The key constraint is then:
for i in (1..n) scalar(A[i],v) <= n
This means that for a given value of i, we can select vertex i but none of the
vertices adjacent to i, or we can reject vertex i and select vertices adjacent
to vertex i. This model is essentially the same as used in triangle packing,
therefore we might hope that we will see the same phase transition behaviour
in SCIP and CP for indSet as for triangle packing.
The decision problem
--------------------
We can generate random graphs G(n,p) where n is number of vertices and p is
edge probability. For a given pair of values (n,p) we can then ask "is there
an independent set of size k?". As we increase k we should move from the
soluble range to the insoluble range. Alternatively for given (n,k) we can
vary p.
Benchmarks
----------
There are DIMACS benchmarks, copied here
http://www.dcs.gla.ac.uk/~pat/jchoco/independentSet/
Patrick
----
Patrick Prosser tel: +44 141 330 4934
Computing Science fax: +44 141 330 4913
17 Lilybank Gardens web: http://www.dcs.gla.ac.uk/~pat/
Glasgow G12 0HE