/* Copyright (C) 2000 Dale Schuurmans, Finnegan Southey */ /* This work is licensed under the Gnu General Public License (see gpl.txt). */ #include #include #include "readcnf.h" #include "satfront.h" int numsat, flips, r; int *make; int *brake; int *maxxs; int *sat; int *timestamp; void preSolve(SATParams *params) { make = malloc((n+1) * sizeof(int)); brake = malloc((n+1) * sizeof(int)); maxxs = malloc((n+1) * sizeof(int)); sat = malloc(m * sizeof(int)); timestamp = malloc((n+1) * sizeof(int)); } /************************ HSAT **********************/ void runSolver(SATParams *params, SATResults *results) { int t, x, y, i, j, nmxs, maxdiff, curdiff, xflip = -1, temp, oldest, currage; int R; int T; #include "mobility1.c" T = params->intParams[0]; R = params->intParams[1]; if (T == 0) T = 100000; if (R == 0) R = 5; flips = 0; for (r = 0; r < R; r++) { /***************************/ for (x = 1; x <= n; x++) assign[x] = (rand()%100 < 50) * 2 - 1; flips++; numsat = 0; for (y = 0; y < m; y++) { sat[y] = 0; for (i=0; i 0; } for (x = 1; x <= n; x++) { timestamp[x] = -1; make[x] = brake[x] = 0; for (j = 0; j < nYs[x]; j++) { if (sat[Ys[x][j]] == 0) make[x]++; else if (sat[Ys[x][j]] == 1 && assign[x] == Ysgns[x][j]) brake[x]++; } } for (t = 0; t < T; t++) { /***************************/ if (numsat == m) break; #include "unsat1.c" #include "mobility2.c" #include "assigndump.c" maxdiff = -m; oldest = t; nmxs = 0; for (x = 1; x <= n; x++) if ((curdiff = make[x]-brake[x]) > maxdiff) { maxdiff = curdiff; maxxs[0] = x; nmxs = 1; oldest = timestamp[x]; } else if (curdiff == maxdiff) { if ((currage = timestamp[x]) < oldest) { maxxs[0] = x; nmxs = 1; oldest = timestamp[x]; } else if (currage == oldest) maxxs[nmxs++] = x; } xflip = maxxs[rand()%nmxs]; timestamp[xflip] = t; assign[xflip] = -assign[xflip]; flips ++; temp = make[xflip]; make[xflip] = brake[xflip]; brake[xflip] = temp; for (j = 0; j < nYs[xflip]; j++) { y = Ys[xflip][j]; if (assign[xflip] != Ysgns[xflip][j]) { if (--sat[y] == 0) { numsat--; for (i = 0; i < nXs[y]; i++) if (Xsgns[y][i] != assign[x=Xs[y][i]] && x != xflip) make[x]++; } else if (sat[y] == 1) for (i = 0; i < nXs[y]; i++) if (Xsgns[y][i] == assign[x=Xs[y][i]] && x != xflip) brake[x]++; } else { if (++sat[y] == 1) { numsat++; for (i = 0; i < nXs[y]; i++) if (Xsgns[y][i] != assign[x=Xs[y][i]] && x != xflip) make[x]--; } else if (sat[y] == 2) for (i = 0; i < nXs[y]; i++) if (Xsgns[y][i] == assign[x=Xs[y][i]] && x != xflip) brake[x]--; } } /* if (maxdiff < 0) printf("step down!\n"); if (maxdiff < 0) break; */ } /***************************/ if (numsat == m) break; } /***************************/ if (numsat != m) r--; results->numFlips = flips; results->numRestarts = r + 1; results->numSatisfied = numsat; results->isSatisfied = numsat == m; results->numClauses = m; #include "mobility3.c" } void postSolve(SATParams *params) { free(make); free(brake); free(maxxs); free(sat); free(timestamp); } SATParams *getSATParams() { SATParams *params; params = malloc(sizeof(SATParams)); params->numIntParams = 2; params->intParams = malloc(params->numIntParams * sizeof(int)); params->intParamNames = malloc(params->numIntParams * sizeof(char*)); params->intParamDescs = malloc(params->numIntParams * sizeof(char*)); params->intParamNames[0] = "-mf"; params->intParamDescs[0] = "max flips before restarting"; params->intParams[0] = 0; params->intParamNames[1] = "-mr"; params->intParamDescs[1] = "max restarts before aborting"; params->intParams[1] = 0; params->numDoubleParams = 0; params->numStringParams = 0; return params; } char *getSolverIdentity() { return "\$RCSfile: hsat.c,v \$ \$Revision: 1.14 \$ \$Date: 2000/12/10 06:03:56 \$"; }