contrib/luby.c

   1 // luby.c - Luby sequence generator
   2 // Morgan Deters <mdeters@cs.nyu.edu> for the CVC4 project, 5 May 2011
   3 //
   4 // This program enumerates the Luby-based MiniSat 2 restart sequence.
   5 // MiniSat restarts after a number of conflicts determined by:
   6 //
   7 //    restart_base * luby(restart_inc, curr_restarts)
   8 //
   9 // By default, MiniSat has restart_base = 25, restart_inc = 3.0, and
  10 // curr_restarts is the number of restarts that have been done (so it
  11 // starts at 0).
  12 //
  13 // For the Luby paper, see:
  14 //   http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.5558
  15 //
  16 // Compile luby.c with gcc -o luby luby.c -lm
  17 //
  18
  19 #include <stdio.h>
  20 #include <stdlib.h>
  21 #include <string.h>
  22 #include <assert.h>
  23 #include <math.h>
  24
  25 // luby() function copied from MiniSat 2
  26 // Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
  27 // Copyright (c) 2007-2010, Niklas Sorensson
  28 double luby(double y, int x){
  29
  30     // Find the finite subsequence that contains index 'x', and the
  31     // size of that subsequence:
  32     int size, seq;
  33     for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1);
  34
  35     while (size-1 != x){
  36         size = (size-1)>>1;
  37         seq--;
  38         x = x % size;
  39     }
  40
  41     return pow(y, seq);
  42 }
  43
  44 int main(int argc, char *argv[]) {
  45   int N;
  46   int base;
  47   double inc;
  48   int i;
  49
  50   if(argc != 4) {
  51     fprintf(stderr, "usage: %s base inc N\n"
  52             "In MiniSat 2, base==25 and inc==3 by default.\n"
  53             "base is simply a multiplier after the sequence is computed.\n"
  54             "N is the number to produce (-1 means run until CTRL-C)\n",
  55             argv[0]);
  56     exit(1);
  57   }
  58
  59   base = atoi(argv[1]);
  60   inc = strtod(argv[2], NULL);
  61   N = atoi(argv[3]);
  62
  63   assert(base >= 1);
  64   assert(inc >= 1.0);
  65
  66   for(i = 0; N < 0 || i < N; ++i) {
  67     printf("%d %f\n", i, luby(inc, i) * base);
  68   }
  69 }