University Homepage School Homepage School Contacts School Search

Assignment 2a: Finding the phase transition (BDD)

Issued 28 January; Handin 12.00 midday, 6 February

Introduction

In this assignment you will gain some familiarity with the ML interface to the BDD package and experiment with this package.

Tasks

1. Write an ML program to create BDDs by repeatedly generating and conjoining random 3-SAT clauses, using a given number N of variables.
2. Instrument your program to collect data on the way the size of the BDD, and the time taken to add each new clause, vary as the number of clauses increases. Experiment with various numbers of variables.
3. Investigate the BDD reordering methods provided by the package to see how they affect these results.
4. Use your results to plot an experimental phase transition graph, for various numbers of variables.

---

Instructions

Use the command ~mfourman/bin/propsat

Then type the following code:

structure Bdd = LOGIC();
open Bdd;
bdd_start();

Here is a small example program you can type interactively to get you started:

val ff = FALSE(); (* the zero BDD *)
val a = V(NEW()); (* NEW() creates a variable *)
SIZE a; (* V builds the corresponding three-node BDD *) val b = V(NEW());
val c = V(NEW());
val x = ORL[++a, ++b, NOT (++c)];
SIZE x;
x = ff;
val y = ++x AND ANDL[NOT (++a), NOT (++b), ++c];
SIZE y;
y = ff;

Hints

Make a function that takes a number, N, and creates a list of N variables.
Select variables randomly from this list using the library function List.nth, and the following pseudo-random number generator generator:

(* Given a seed, mkRandom returns a psuedo-random number generator
which takes an integer argument of one more than the maximum
return value required. ( Linear Congruential, after Sedgewick,
"Algorithms", Addison-Wesley, 1983, Chapter 3 pp 37-38.) *)

fun mkRandom seed =
let val r = ref seed
val a = 31415821
val m = 100000000

fun f n =
let val rand = (r := ((a * !r + 1) mod m);
(!r * n) div m)
in if n < 0 then rand + 1 else rand
end
in f
end;


---

Author: Michael Fourman
Revision 1.1 by neilb
2004/08/09 22:04:03