1 // luby.c - Luby sequence generator
2 // Morgan Deters <mdeters@cs.nyu.edu> for the CVC4 project, 5 May 2011
4 // This program enumerates the Luby-based MiniSat 2 restart sequence.
5 // MiniSat restarts after a number of conflicts determined by:
7 // restart_base * luby(restart_inc, curr_restarts)
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
13 // For the Luby paper, see:
14 // http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.5558
16 // Compile luby.c with gcc -o luby luby.c -lm
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
){
30 // Find the finite subsequence that contains index 'x', and the
31 // size of that subsequence:
33 for (size
= 1, seq
= 0; size
< x
+1; seq
++, size
= 2*size
+1);
44 int main(int argc
, char *argv
[]) {
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",
60 inc
= strtod(argv
[2], NULL
);
66 for(i
= 0; N
< 0 || i
< N
; ++i
) {
67 printf("%d %f\n", i
, luby(inc
, i
) * base
);