/* Copyright (C) 2000 Dale Schuurmans, Finnegan Southey */ /* This work is licensed under the Gnu General Public License (see gpl.txt). */ /* Multiplicative updates, using our standard hinge penalty */ /* Note: For our SAT BLP formulation, a variable satisfies a clause when the * value of the variable is _not_ equal to the corresponding coefficient. * i.e. X[Xs[c][i]] != Xcoefs[c][i] * When not equal, the violation value is decreased. * When equal, the violation value is increased. */ #include #include #include #include #include #include #include "cop.h" #include "satfront.h" /* Macros. */ #define swapint(x,y) {tempint=x; x=y; y=tempint;} #define swapreal(x,y) {tempreal=x; x=y; y=tempreal;} /* Default parameter values. */ #define DEFAULT_MAX_STEPS 500000 #define DEFAULT_MAX_TRIES 1 #define DEFAULT_ALPHA 0.995 #define DEFAULT_RAW_ALPHA 0.25 #define DEFAULT_RHO 0.99 #define DEFAULT_CORR 100 #define DEFAULT_WALK_PROB 0.002 /* Defines for dumping weight vector and violation profiles. */ #define USE_WEIGHT_TRACKING 0 #define WEIGHT_FILE_EXT ".wei" #define VIOLATION_FILE_EXT ".vio" /* Defines for dumping/reading/randomizing initial/average/last weight vectors. */ #define DUMP_WEIGHT_AVG 0 #define READ_WEIGHTS 0 #define RANDOMIZE_WEIGHTS 0 #define NORMALIZE_WEIGHTS_ON_READ 1 #define AVG_FILE_EXT ".avg" #define LAST_WEIGHTS_FILE_EXT ".lstw" #define LAST_ASG_FILE_EXT ".lstx" /* Allows us to change floating-point type easily. */ typedef double REAL; /* Function prototypes. */ double obval(); double weightMagSqr(); void startWeightTracking(SATParams *params); void dumpWeightAverages(SATParams *params); void dumpFinalWeights(SATParams *params); void dumpFinalAssigns(SATParams *params); void readWeights(SATParams *params, REAL *weights); void readAssigns(SATParams *params, int *assigns); void randomizeWeights(SATParams *params, REAL *weights); /* Corrections * * This implementation uses lazy updates of weights and weighted values. * Since weights are only changed on dual steps, the lagged effects of weight * updates are determined by keeping track of the number of dual steps * since a weight's real value was updated. Precomputed tables mean that * the weight's value can be computed efficiently, but only within the * "window" allowed by the size of the tables. * The length of the window is determined by the correction period. * Every "corr" number of dual steps, a correction is performed to account * for numerical drift. At this correction, all weights are brought up to * date, so no tables longer than the correction period is necessary. * Comments in this source refer to this overal concept as the "Dual Window". */ /* Smoothing * * Note that the ESG algorithm states that smoothing is "the adjustment * of the weights towards the population mean of the weights". * We now use an approximation of this. Weights are set to 1, and are * smoothed towards 1, instead of the population mean. * This has the desired smoothing effect and does not appear to change the * behaviour of the algorithm. The overall result is a much * faster implementation and improved numerical stability. */ int corr; /* Parameter: Dual steps per correction. */ REAL alpha; /* Parameter: Weight update step size. */ REAL rho; /* Parameter: Smoothing rate. */ int W; /* Parameter: Walk probability. */ int tempint; /* Temp var. */ REAL tempreal; /* Temp var. */ REAL rhoalpha; /* rho * alpha */ REAL oneminusrho; /* 1 - rho */ int R; /* Restart loop counter. */ int T; /* Flip loop counter. */ int *vio; /* Number of constraints violated by flipping a var [var]. */ int *sat; /* Number of constraints satisfied by flipping a var [var]. */ int *V; /* Violation value for each constraint. > 0 -> violated [constraint] */ REAL *Y; /* Weight for each constraint [constraint]. */ /* Variables for tracking violated constraints. */ int numvio; /* Number of violated constraints. */ int *cviol; /* List of violated constraint indices. [list index] */ int *wherecviol; /* Index of constraint in cviol (only valid if it's actually in the list) [constraint]. */ /* Variables for tracking variables that will satisfy constraints when * flipped (violation reducers). */ int nxvr; /* Number of violation reducers. */ int *xvreducers; /* List of violation reducers [list index]. */ int *wherexvreduce; /* Index of var in xvreducers (only valid if it's actually in the list) [var]. */ /* Variables for tracking list of candidates to flip in primal step. */ int nmxs; /* Number of candidates in flip minxs. */ int *minxs; /* List of candidates to flip [list index]. */ /* Timestamp variables. */ int *dtime; /* Time a constraint was last updated [constraint]. */ int *xup2time; /* Time when Yup2 for a var was last updated. [var] */ int *xdn3time; /* Time when Ynd3 for a var was last updated. [var] */ /* Lagrange objective change trackers (increases, decreases, and net change). */ REAL *Yup2; /* Total weight increase from flipping a var [var]. */ REAL *Ydn3; /* Total weight decrease from flipping a var [var]. */ REAL *diffL; /* Net change in Lagrange from flipping var (only maintained for xvreducers)[var]. */ /* Precomputed tables of powers. */ REAL *rhoalphapow; /* Precomputed table of powers of rho*alpha. [power]*/ REAL *rhopow; /* Precomputed table of powers of rho. [power] */ REAL *viosmooth; /* Table for smoothing vio constraints . [dual steps] */ REAL *satsmooth; /* table for smoothing sat constraints. [dual steps] */ /* File pointers used for weight tracking (if enabled). */ #if USE_WEIGHT_TRACKING FILE *weightFile = NULL; FILE *vioFile = NULL; #endif /* Used in optional weight average computation. */ REAL *weightSums; int weightUpdates = 0; void preSolve(SATParams *params) { int d; double scaledalpha, rawalpha, walkprob; REAL vioconst; /* (1 - rho) / (1 - rho*alpha) */ /* Get parameter values. */ T = params->intParams[0]; if (T == 0) T = DEFAULT_MAX_STEPS; R = params->intParams[1]; if (R == 0) R = DEFAULT_MAX_TRIES; corr = params->intParams[2]; if (corr == 0) corr = DEFAULT_CORR; scaledalpha = params->doubleParams[0]; rawalpha = params->doubleParams[3]; if (scaledalpha != 0 && rawalpha != 0) { fprintf(stderr, "Cannot specify both '-alpha' and '-rawalpha' ('alpha' is a scaled version of 'rawalpha')\n"); exit(EXIT_FAILURE); } /* By default, we will use scaled "alpha". */ /* This scaling is based on limited experimentation and has limited * justification. However, the "alphas" reported in our IJCAI'01 paper * are scaled in this fashion. */ if (scaledalpha == 0 && rawalpha == 0) { /* Use default value for alpha scaled by problem size. */ alpha = 1.0 + DEFAULT_ALPHA * n / (REAL)m; } else if (scaledalpha != 0) { /* A scaled alpha was specified. */ alpha = 1.0 + scaledalpha * n / (REAL)m; } else { /* A raw alpha was specified. */ alpha = rawalpha; } rho = params->doubleParams[1]; if (rho == 0) rho = DEFAULT_RHO; oneminusrho = 1 - rho; walkprob = params->doubleParams[2]; if (walkprob == 0) walkprob = DEFAULT_WALK_PROB; W = RAND_MAX * walkprob; if (MaxCoef > 1) { printf("Error: this implementation assumes {-1,0,+1} valued "); printf("coefficients\n"); exit(EXIT_FAILURE); } /* Allocate lots of memory. */ sat = (int *) malloc(n * sizeof(int)); vio = (int *) malloc(n * sizeof(int)); xvreducers = (int *) malloc(n * sizeof(int)); minxs = (int *) malloc(n * sizeof(int)); wherexvreduce = (int *) malloc(n * sizeof(int)); cviol = (int *) malloc(m * sizeof(int)); wherecviol = (int *) malloc(m * sizeof(int)); V = (int *) malloc(m * sizeof(int)); dtime = (int *) malloc(m * sizeof(int)); Y = (REAL *) malloc(m * sizeof(REAL)); diffL = (REAL *) malloc(n * sizeof(REAL)); Yup2 = (REAL *) malloc(n * sizeof(REAL)); Ydn3 = (REAL *) malloc(n * sizeof(REAL)); xup2time = (int *) malloc(n * sizeof(int)); xdn3time = (int *) malloc(n * sizeof(int)); rhoalphapow = (REAL *) malloc(corr * sizeof(REAL)); rhopow = (REAL *) malloc(corr * sizeof(REAL)); viosmooth = (REAL *) malloc(corr * sizeof(REAL)); satsmooth = (REAL *) malloc(corr * sizeof(REAL)); rhoalphapow[0] = 1.0; rhopow[0] = 1.0; rhoalpha = rho * alpha; vioconst = oneminusrho / (1.0 - rhoalpha); viosmooth[0] = 0.0; satsmooth[0] = 0.0; /* Compute lookup table for lazy updates. * Powers of rho and rhoalpha, and smoothing factors. */ for (d = 1; d < corr; d++) { rhopow[d] = rhopow[d-1] * rho; rhoalphapow[d] = rhoalphapow[d-1] * rhoalpha; satsmooth[d] = 1.0 - rhopow[d]; viosmooth[d] = vioconst * (1.0 - rhoalphapow[d]); } #if DUMP_WEIGHT_AVG weightSums = calloc(m, sizeof(REAL)); #endif } void runSolver(SATParams *params, SATResults *results) { /* Varying throughout run. */ int x; /* Index/counter used for variables. */ int c; /* Index/counter used for constraints. */ int i, j; /* Index/counter used for miscellaneous loops. */ int t; /* Step counter (primal and dual). */ int xflip; /* Index of variable to be flipped. */ REAL mindiff; /* Used to track candidates for flipping. */ int d; /* Dual Window Timer: Dual steps since last correction. */ /* Vars used to cache results for speed. */ int Vc, dtimec, *px; #include "mobility1.c" #if USE_WEIGHT_TRACKING startWeightTracking(params); #endif steps = 0; dsteps = 0; /* For each restart... */ for (r = 0; r < R; r++) { /*******************************************/ /* Create random variable assignment. */ for (x = 0; x < n; x++) X[x] = (rand() < HALF_RAND_MAX) ? -1 : 1; /* We consider the initial assignment to be a "step". */ steps++; numvio = 0; /* For each constraint... */ for (c = 0; c < m; c++) { /* Determine the violation of the constraint given the assignment. */ V[c] = -B[c]; for (i = 0; i < nXs[c]; i++) V[c] += X[Xs[c][i]] == Xcoefs[c][i] ? 1 : -1; /* If constraint is violated, add it to the list of violated * constraints. */ if (V[c] > 0) { cviol[numvio] = c; wherecviol[c] = numvio; numvio++; } /* Out SAT BLP formulation gives violation levels that differ by two, so * we divide by two to make it a little more intuitive. */ V[c] /= 2; /* Set initial constraint weight. */ Y[c] = 1.0; /* Initialize timestamp on each constraint. */ dtime[c] = 1; } #if READ_WEIGHTS /* This allows us to initialize the weight vector from a file. */ readWeights(params, Y); #endif #if RANDOMIZE_WEIGHTS /* This allows us to initialize the weight vector randomly. */ randomizeWeights(params, Y); #endif #if USE_WEIGHT_TRACKING fprintf(weightFile, "%d\t%d", 0, numvio); for (j = 0; j < m; j++) { fprintf(weightFile, "\t%g", Y[j]); } fprintf(weightFile, "\n"); fprintf(vioFile, "%d\t%d", 0, numvio); for (j = 0; j < m; j++) { fprintf(vioFile, "\t%d", V[j]); } fprintf(vioFile, "\n"); #endif #if DUMP_WEIGHT_AVG for (j = 0; j < m; j++) weightSums[j] += Y[j]; weightUpdates++; #endif /* Initialize dual window timer and timestamps. */ d = 1; nxvr = 0; /* For each variable... */ for (x = 0; x < n; x++) { sat[x] = 0; vio[x] = 0; Yup2[x] = 0.0; Ydn3[x] = 0.0; xup2time[x] = 1; xdn3time[x] = 1; /* For each clause in which the variable appears... */ for (j = 0; j < nCs[x]; j++) { c = Cs[x][j]; if (V[c] >= 0) { if (V[c] == 1) { /* Constraint is violated. */ /* Increment count of constraints satisfiable by flipping 'x'. */ sat[x]++; /* Adjust total weight decrease for flipping 'x'. */ Ydn3[x] += Y[c]; /* The first time this variable is known to satisfy a constraint * when flipped, add it to the list of violation reducers. */ if (sat[x] == 1) { xvreducers[nxvr] = x; wherexvreduce[x] = nxvr; nxvr++; } } else { /* Constraint is "satisifed". */ /* V[c] == 0 */ if (X[x] != Ccoefs[x][j]) { /* Constraint is "satisifed" only by 'x'. */ /* Increment count of constraints violated by flipping 'x'. */ vio[x]++; /* Adjust total weight increase for flipping 'x'. */ Yup2[x] += Y[c]; } } } } /* If x an xvreducer then calculate improvement for flipping it */ if (sat[x] > 0) diffL[x] = Yup2[x] - Ydn3[x]; } /* For each step (primal or dual)... */ for (t = 0; t < T; t++) { /***************************/ /* Allows mobility tracking (if enabled in satfront.h). */ #include "mobility2.c" /* Allows unsat clause tracking (if enabled in satfront.h). */ #include "unsat1.c" /* Allows assignment tracking (if enabled in satfront.h). */ #include "assigndump.c" /* If no constraints are violated, then we are finished. */ if (numvio == 0) break; /* If 'corr' dual steps have elapsed, perform a correction. */ if (d % corr == 0) { /* For each constraint... */ for (c = 0; c < m; c++) { /* Cache timestamp on constraint. */ dtimec = dtime[c]; /***** Synchronize Y[c] *****/ /* If constraint needs updating... */ if (dtimec < d) { /* Constraint needs updating. */ if (V[c] > 0) { /* Constraint is violated. */ /* Update weight of 'c'. */ Y[c] = Y[c] * rhoalphapow[d - dtimec] + viosmooth[d - dtimec]; } else { /* Constraint is satisfied. */ /* Update weight of 'c'. */ Y[c] = Y[c] * rhopow[d - dtimec] + satsmooth[d - dtimec]; } } dtime[c] = 1; } /* Restart the dual window timer. */ d = 1; /* For each variable... */ for (x = 0; x < n; x++) { int *Csx, *Ccoefsx, Xx; /* Zero flip effects. */ Yup2[x] = 0.0; Ydn3[x] = 0.0; /* Reset timestamps. */ xup2time[x] = 1; xdn3time[x] = 1; /* Cache some values for speed. */ Csx = Cs[x]; Ccoefsx = Ccoefs[x]; Xx = X[x]; /* Now recompute flip effects on weight for each variable. */ /* IDEA: Use pointer crawling. */ for (j = 0; j < nCs[x]; j++) { c = Csx[j]; if (V[c] >= 0) { if (V[c] == 1) { /* Constraint is violated. */ Ydn3[x] += Y[c]; } else { /* Constraint is satisfied by one variable. */ if (Xx != Ccoefsx[j]) { /* 'x' satisfies the constraint. */ Yup2[x] += Y[c]; } } } } /* If x an xvreducer then calculate improvement for flipping it */ if (sat[x] > 0) diffL[x] = Yup2[x] - Ydn3[x]; } } /* End of correction. */ /* Find candidates to flip. */ mindiff = DBL_MAX; nmxs = 0; /* For each xvreducer... */ for (px = xvreducers; px < xvreducers+nxvr; px++) { x = *px; /* Track variable that gives the greatest improvement. */ if (diffL[x] <= mindiff) { if (diffL[x] < mindiff) { mindiff = diffL[x]; minxs[0] = x; nmxs = 1; } else minxs[nmxs++] = x; } } /* Pick variable that most improves objective (break ties randomly). * If no variable improves objective, check walk probability for a * random flip. If we do not perform a random walk, perform a dual * step. */ if (mindiff < 0.0) { /* If there is only one candidate, pick that, otherwise pick * randomly. */ if (nmxs == 1) xflip = minxs[0]; else xflip = minxs[rand()%nmxs]; } else if (random() < W) { xflip = rand() % n; /* If the randomly selected xflip is not an xvreducer * (sat[xflip]==0) and flipping it will violate one or more * constraints (vio[xflip]>0), then we must add it to the list of * xvreducers since the primal step will not handle it in * this specific case. */ if (vio[xflip] > 0 && sat[xflip] == 0) { xvreducers[nxvr] = xflip; wherexvreduce[xflip] = nxvr; nxvr++; diffL[xflip] = Yup2[xflip] - Ydn3[xflip]; } } else { /* Set xflip to -1 to indicate that no primal step offers * improvement so we should do a dual step. */ xflip = -1; } /* If no variable flip was selected, perform a dual step, otherwise * perform a primal step. */ if (xflip == -1) { /*** DUAL STEP ***/ /* Note that we don't update any of the actual weights. These * updates are performed lazily (on demand) or when a correction is * performed. We only update various totals and some key values * required to compute the objective value of neighbours. * * The hinge penalty means we increase the weight of violated * constraints but leave satisfied constraints unchanged. * Moreover, in the SAT BLP formulation, the violation value for * violated constraints is always 1. So we simply multiply by * alpha. */ /* Increment dual step counter. */ dsteps++; /* Increment Dual Window timer. */ d++; /* For each violation reducer... */ for (i = 0; i < nxvr; i++) { x = xvreducers[i]; /* Update weight changes due to flipping. */ Yup2[x] = rho * Yup2[x] + oneminusrho * vio[x]; Ydn3[x] = rhoalpha * Ydn3[x] + oneminusrho * sat[x]; /* Update time stamps. */ xup2time[x] = d; xdn3time[x] = d; /* Update overall change. */ diffL[x] = Yup2[x] - Ydn3[x]; } #if USE_WEIGHT_TRACKING fprintf(weightFile, "%d\t%d", t, numvio); for (j = 0; j < m; j++) { fprintf(weightFile, "\t%g", Y[j]); } fprintf(weightFile, "\n"); fprintf(vioFile, "%d\t%d", t, numvio); for (j = 0; j < m; j++) { fprintf(vioFile, "\t%d", V[j]); } fprintf(vioFile, "\n"); #endif #if DUMP_WEIGHT_AVG for (j = 0; j < m; j++) weightSums[j] += Y[j]; weightUpdates++; #endif } else { /* Variables to cache values. */ int Xxflip; int *Ccoefsxflip, *Csxflip; /*** PRIMAL STEP ***/ /* Perform the actual flip and cache the new value for speed. */ Xxflip = -X[xflip]; X[xflip] = Xxflip; /* Swap various values offered by flipping. */ swapreal(Yup2[xflip], Ydn3[xflip]); swapint(xup2time[xflip], xdn3time[xflip]); swapint(sat[xflip], vio[xflip]); /* Negate the change in L offered by flipping. */ diffL[xflip] = -diffL[xflip]; /* If the variable is in the xvreducers list (vio[xflip]>0) and will * no longer satisfy a constraint if flipped (sat[xflip==0), then we * must remove it from the xvreducers list. */ if (sat[xflip] == 0 && vio[xflip] > 0) { nxvr--; xvreducers[wherexvreduce[xflip]] = xvreducers[nxvr]; wherexvreduce[xvreducers[nxvr]] = wherexvreduce[xflip]; } /* Increment primal step count. */ steps++; /* Cache some array indexing for speed. */ Ccoefsxflip = Ccoefs[xflip]; Csxflip = Cs[xflip]; /* For each constraint in which 'xflip' appears... */ for (j = 0; j < nCs[xflip]; j++) { /* Variables for caching results. */ int *Xsc; int *Xcoefsc; /* Cache some values and arrays for speed. */ /* Note: Vc is the violation level of 'c' before the flip. */ c = Csxflip[j]; Vc = V[c]; Xsc = Xs[c]; Xcoefsc = Xcoefs[c]; dtimec = dtime[c]; /***** Synchronize Y[c] *****/ /* Peform the required lazy update on the weight of 'c'. */ /* This is essentially the same as the update performed during the * correction. See that code for details. */ if (dtimec < d) { if (Vc > 0) { Y[c] = Y[c]*rhoalphapow[d-dtimec] + viosmooth[d-dtimec]; } else { Y[c] = Y[c]*rhopow[d-dtimec] + satsmooth[d-dtimec]; } dtime[c] = d; } if (Xxflip == Ccoefsxflip[j]) { /* 'xflip' no longer satisfies constraint. */ if (Vc == -1) { /* CASE A: Constraint was satisfied by two vars (now one). */ /* Search for the one remaining satisfying variable. */ x = *Xsc; while (X[x] == *Xcoefsc) { Xcoefsc++; Xsc++; x = *Xsc; } /* Update the remaining satifying variable ('x'). */ /***** Synchronize Yup2[x] *****/ /* Updates Yup2[x] to reflect all weight changes since it * was last updated. */ if (xup2time[x] < d) { Yup2[x] = Yup2[x] * rhopow[d - xup2time[x]] + satsmooth[d - xup2time[x]] * vio[x]; xup2time[x] = d; } /* Increment count of constraints violated by flipping 'x'. */ vio[x]++; /* Adjust total weight increase for flipping 'x'. */ Yup2[x] += Y[c]; /* If 'x' is an xvreducer (sat[x]>0) then we maintain diffL ... */ /* Adjust net change for flipping variable 'x'. */ if (sat[x]) diffL[x] += Y[c]; /* End of CASE A. */ } else if (Vc == 0) { /* CASE B: Constraint was satisfied by one var (now zero). */ /* Add constraint to list of violated constraints. */ cviol[numvio] = c; wherecviol[c] = numvio; numvio++; /* For each variable in the constraint... */ for (i = 0; i < nXs[c]; i++) { x = Xsc[i]; /* The following update should only be performed for * non-satisfying variables that are not 'xflip'. Since no * variables satisfy this constraint, we need only check * that 'x!=xflip'. */ if (x != xflip) { /* 'x' is not 'xflip' and does not satisfy the constraint. */ /***** Synchronize Ydn3[x] *****/ if (xdn3time[x] < d) { Ydn3[x] = Ydn3[x] * rhoalphapow[d - xdn3time[x]] + viosmooth[d - xdn3time[x]] * sat[x]; xdn3time[x] = d; } /* Increment number of constraints satisfied by flipping 'x'. */ sat[x]++; /* Adjust total weight decrease for flipping 'x'. */ Ydn3[x] += Y[c]; /* If this variable is newly able to satisfy a constraint * when flipped, add it to the list of violation reducers. */ if (sat[x] == 1) { /***** Synchronize Yup2[x] *****/ if (xup2time[x] < d) { Yup2[x] = Yup2[x] * rhopow[d - xup2time[x]] + satsmooth[d - xup2time[x]] * vio[x]; xup2time[x] = d; } /* Add to list of violation reducers. */ xvreducers[nxvr] = x; wherexvreduce[x] = nxvr; nxvr++; } /* This variable must be an xvreducer (sat[x] > 0) so we * must maintain diffL. */ /* Adjust overall improvement for flipping variable 'x'. */ diffL[x] = Yup2[x] - Ydn3[x]; } } /* End of CASE B. */ } /* Increase violation level of constraint. */ V[c] += 1; /* End of "xflip no longer satisfies constraint". */ } else { /* 'xflip' now satisfies constraint. */ /* We are interested in two cases, (Vc == 0) (Case C) * and (Vc == 1) (Case D). * Since Vc is never > 1, we can use the following * check to avoid a redundant comparison. */ if (Vc >= 0) { if (Vc == 0) { /* CASE C: Constraint was satisfied by one var (now two). */ x = *Xsc; while (X[x] == *Xcoefsc || x == xflip) { Xsc++; Xcoefsc++; x = *Xsc; } /* 'x' is not 'xflip' and satisfies the constraint. */ /***** Synchronize Yup2[x] *****/ if (xup2time[x] < d) { Yup2[x] = Yup2[x] * rhopow[d - xup2time[x]] + satsmooth[d - xup2time[x]] * vio[x]; xup2time[x] = d; } /* Decrement count of constraints violated by flipping 'x'. */ vio[x]--; /* Adjust total weight decrease for flipping 'x'. */ Yup2[x] -= Y[c]; /* If 'x' is an xvreducer (sat[x]>0) then we maintain diffL ... */ /* Adjust net change for flipping variable 'x'. */ if (sat[x]) diffL[x] -= Y[c]; /* End of CASE C. */ } else { /* (Vc == 1). */ /* CASE D: Constraint was violated (now satisfied by one). */ /* Remove constraint from violated constraint list. */ numvio--; cviol[wherecviol[c]] = cviol[numvio]; wherecviol[cviol[numvio]] = wherecviol[c]; for (i = 0; i < nXs[c]; i++) { x = Xsc[i]; /* Update all variables except for 'xflip'. */ if (x != xflip) { /* 'x' is not 'xflip' and does not satisfy the constraint. */ /***** Synchronize Ydn3[x] *****/ if (xdn3time[x] < d) { Ydn3[x] = Ydn3[x] * rhoalphapow[d - xdn3time[x]] + viosmooth[d - xdn3time[x]] * sat[x]; xdn3time[x] = d; } /* Decrement number of constraints satisfied by flipping 'x'. */ sat[x]--; /* Adjust total weight increase for flipping 'x'. */ Ydn3[x] -= Y[c]; /* If flipping 'x' will no longer satisfy any constraints, * remove it from the list of xvreducers, * otherwise, we must maintain diffL so adjust overall * degradation. */ if (sat[x] == 0) { nxvr--; xvreducers[wherexvreduce[x]] = xvreducers[nxvr]; wherexvreduce[xvreducers[nxvr]]=wherexvreduce[x]; } else diffL[x] += Y[c]; } } } /* End of CASE D. */ } /* End of (Vc >= 0). */ /* Reduce violation level of the constraint. */ V[c] -= 1; } /* End of "xflip now satisfies constraint". */ } /* End of constraint update. */ } /* End of PRIMAL STEP. */ } /* End of step loop. */ /* If no constraints are violated, then we are finished. */ if (numvio == 0) break; } /* End of restart loop. */ if (numvio > 0) r--; results->numFlips = steps; results->numReweights = dsteps; results->numRestarts = r + 1; results->numSatisfied = m - numvio; results->isSatisfied = numvio == 0; #include "copysoln.c" #include "mobility3.c" } void postSolve(SATParams *params) { free(Y); free(V); free(diffL); free(minxs); free(sat); free(vio); free(xvreducers); free(wherexvreduce); free(cviol); free(wherecviol); free(dtime); free(Yup2); free(Ydn3); free(xup2time); free(xdn3time); free(rhoalphapow); free(rhopow); free(viosmooth); free(satsmooth); #if USE_WEIGHT_TRACKING fclose(weightFile); fclose(vioFile); #endif #if DUMP_WEIGHT_AVG dumpWeightAverages(params); dumpFinalWeights(params); dumpFinalAssigns(params); free(weightSums); #endif } SATParams *getSATParams() { SATParams *params; params = malloc(sizeof(SATParams)); params->numIntParams = 3; 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->intParamNames[2] = "-cp"; params->intParamDescs[2] = "number of reweights between corrections"; params->intParams[2] = 0; params->numDoubleParams = 4; params->doubleParams = malloc(params->numDoubleParams * sizeof(double)); params->doubleParamNames = malloc(params->numDoubleParams * sizeof(char*)); params->doubleParamDescs = malloc(params->numDoubleParams * sizeof(char*)); params->doubleParamNames[0] = "-alpha"; params->doubleParamDescs[0] = "scaled reweight step size (1+alpha*n/m)"; params->doubleParams[0] = 0; params->doubleParamNames[1] = "-rho"; params->doubleParamDescs[1] = "rate of weight shrinkage to mean for sat clauses"; params->doubleParams[1] = 0; params->doubleParamNames[2] = "-noise"; params->doubleParamDescs[2] = "probability of random walk when stuck"; params->doubleParams[2] = 0; params->doubleParamNames[3] = "-rawalpha"; params->doubleParamDescs[3] = "raw reweight step size (rawalpha)"; params->doubleParams[3] = 0; params->numStringParams = 0; return params; } char *getSolverIdentity() { return "$RCSfile: esg.c,v $ $Revision: 1.66.2.1 $ $Date: 2002/02/07 01:15:53 $"; } double obval() { int c; double val = 0; for (c = 0; c < numvio; c++) { val += Y[cviol[c]]; } return val; } double weightMagSqr() { int y; double mag = 0; for (y = 0; y < m; y++) { mag += Y[y] * Y[y]; } return mag; } void startWeightTracking(SATParams *params) { #if USE_WEIGHT_TRACKING char *fname; fname = malloc(sizeof(char) * strlen(params->shortFilename) + strlen(WEIGHT_FILE_EXT) + 1); strcpy(fname, params->shortFilename); strcat(fname, WEIGHT_FILE_EXT); weightFile = fopen(fname, "w"); if (weightFile == NULL) { fprintf(stderr, "Error opening weight file for writing: %s\n", fname); exit(EXIT_FAILURE); } free(fname); fprintf(weightFile, "%d\n", m); fname = malloc(sizeof(char) * strlen(params->shortFilename) + strlen(VIOLATION_FILE_EXT) + 1); strcpy(fname, params->shortFilename); strcat(fname, VIOLATION_FILE_EXT); vioFile = fopen(fname, "w"); if (vioFile == NULL) { fprintf(stderr, "Error opening vio file for writing: %s\n", fname); exit(EXIT_FAILURE); } free(fname); fprintf(vioFile, "%d\n", m); #endif } void dumpWeightAverages(SATParams *params) { FILE *avgFile; int y; char *fname; fname = malloc(sizeof(char) * strlen(params->shortFilename) + strlen(AVG_FILE_EXT) + 1); strcpy(fname, params->shortFilename); strcat(fname, AVG_FILE_EXT); avgFile = fopen(fname, "w"); if (avgFile == NULL) { fprintf(stderr, "Error opening average file for writing: %s\n", fname); exit(EXIT_FAILURE); } free(fname); fprintf(avgFile, "%d", m); for (y = 0; y < m; y++) { fprintf(avgFile, "\t%lg", weightSums[y] / weightUpdates); weightSums[y] = 0.0; } fclose(avgFile); } void dumpFinalWeights(SATParams *params) { FILE *lastWeightFile; int y; char *fname; fname = malloc(sizeof(char) * strlen(params->shortFilename) + strlen(LAST_WEIGHTS_FILE_EXT) + 1); strcpy(fname, params->shortFilename); strcat(fname, LAST_WEIGHTS_FILE_EXT); lastWeightFile = fopen(fname, "w"); if (lastWeightFile == NULL) { fprintf(stderr, "Error opening last weights file for writing: %s\n", fname); exit(EXIT_FAILURE); } free(fname); fprintf(lastWeightFile, "%d", m); for (y = 0; y < m; y++) { fprintf(lastWeightFile, "\t%lg", Y[y]); } fclose(lastWeightFile); } void dumpFinalAssigns(SATParams *params) { FILE *lastAsgFile; int x; char *fname; fname = malloc(sizeof(char) * strlen(params->shortFilename) + strlen(LAST_ASG_FILE_EXT) + 1); strcpy(fname, params->shortFilename); strcat(fname, LAST_ASG_FILE_EXT); lastAsgFile = fopen(fname, "w"); if (lastAsgFile == NULL) { fprintf(stderr, "Error opening last assignment file for writing: %s\n", fname); exit(EXIT_FAILURE); } free(fname); fprintf(lastAsgFile, "%d", n); for (x = 0; x < n; x++) { fprintf(lastAsgFile, "\t%d", X[x]); } fclose(lastAsgFile); } void readAssigns(SATParams *params, int *assigns) { FILE *asgFile; int x; char *fname; int junk; fname = malloc(sizeof(char) * strlen(params->shortFilename) + strlen(LAST_ASG_FILE_EXT) + 1); strcpy(fname, params->shortFilename); strcat(fname, LAST_ASG_FILE_EXT); asgFile = fopen(fname, "r"); if (asgFile == NULL) { fprintf(stderr, "Error opening assign file for reading: %s\n", fname); exit(EXIT_FAILURE); } free(fname); if (fscanf(asgFile, "%d", &junk) != 1) { fprintf(stderr, "Error reading number of assigns in assign file.\n"); exit(EXIT_FAILURE); } if (junk != n) { fprintf(stderr, "Number of assigns in file does not match number of assigns in current problem.\n"); exit(EXIT_FAILURE); } for (x = 0; x < n; x++) { if (fscanf(asgFile, "%d", assigns + x) != 1) { fprintf(stderr, "Error reading assign in assigns file.\n"); exit(EXIT_FAILURE); } } } void readWeights(SATParams *params, REAL *weights) { FILE *avgFile; int y; char *fname; int junk; REAL total; fname = malloc(sizeof(char) * strlen(params->shortFilename) + strlen(AVG_FILE_EXT) + 1); strcpy(fname, params->shortFilename); strcat(fname, AVG_FILE_EXT); avgFile = fopen(fname, "r"); if (avgFile == NULL) { fprintf(stderr, "Error opening weight file for reading: %s\n", fname); exit(EXIT_FAILURE); } free(fname); if (fscanf(avgFile, "%d", &junk) != 1) { fprintf(stderr, "Error reading number of weights in average file.\n"); exit(EXIT_FAILURE); } if (junk != m) { fprintf(stderr, "Number of weights in file does not match number of weights in current problem.\n"); exit(EXIT_FAILURE); } #if NORMALIZE_WEIGHTS_ON_READ total = 0; for (y = 0; y < m; y++) { if (fscanf(avgFile, "%lg", weights + y) != 1) { fprintf(stderr, "Error reading weight in average file.\n"); exit(EXIT_FAILURE); } total += weights[y]; } for (y = 0; y < m; y++) weights[y] /= total; #else for (y = 0; y < m; y++) if (fscanf(avgFile, "%lg", weights + y) != 1) { fprintf(stderr, "Error reading weight in average file.\n"); exit(EXIT_FAILURE); } #endif fclose(avgFile); } void randomizeWeights(SATParams *params, REAL *weights) { int y; REAL total; total = 0; for (y = 0; y < m; y++) { do { weights[y] = (REAL)rand(); } while (weights[y] == 0.0); total += weights[y]; } #if NORMALIZE_WEIGHTS_ON_READ for (y = 0; y < m; y++) weights[y] /= total; #endif }