diff options
Diffstat (limited to 'src/misc/espresso/pair.c')
| -rw-r--r-- | src/misc/espresso/pair.c | 675 |
1 files changed, 0 insertions, 675 deletions
diff --git a/src/misc/espresso/pair.c b/src/misc/espresso/pair.c deleted file mode 100644 index a8077176..00000000 --- a/src/misc/espresso/pair.c +++ /dev/null @@ -1,675 +0,0 @@ -/* - * Revision Control Information - * - * $Source$ - * $Author$ - * $Revision$ - * $Date$ - * - */ -#include "espresso.h" - -void set_pair(PLA) -pPLA PLA; -{ - set_pair1(PLA, TRUE); -} - -void set_pair1(PLA, adjust_labels) -pPLA PLA; -bool adjust_labels; -{ - int i, var, *paired, newvar; - int old_num_vars, old_num_binary_vars, old_size, old_mv_start; - int *new_part_size, new_num_vars, new_num_binary_vars, new_mv_start; - ppair pair = PLA->pair; - char scratch[1000], **oldlabel, *var1, *var1bar, *var2, *var2bar; - - if (adjust_labels) - makeup_labels(PLA); - - /* Check the pair structure for valid entries and see which binary - variables are left unpaired - */ - paired = ALLOC(bool, cube.num_binary_vars); - for(var = 0; var < cube.num_binary_vars; var++) - paired[var] = FALSE; - for(i = 0; i < pair->cnt; i++) - if ((pair->var1[i] > 0 && pair->var1[i] <= cube.num_binary_vars) && - (pair->var2[i] > 0 && pair->var2[i] <= cube.num_binary_vars)) { - paired[pair->var1[i]-1] = TRUE; - paired[pair->var2[i]-1] = TRUE; - } else - fatal("can only pair binary-valued variables"); - - PLA->F = delvar(pairvar(PLA->F, pair), paired); - PLA->R = delvar(pairvar(PLA->R, pair), paired); - PLA->D = delvar(pairvar(PLA->D, pair), paired); - - /* Now painfully adjust the cube size */ - old_size = cube.size; - old_num_vars = cube.num_vars; - old_num_binary_vars = cube.num_binary_vars; - old_mv_start = cube.first_part[cube.num_binary_vars]; - /* Create the new cube.part_size vector and setup the cube structure */ - new_num_binary_vars = 0; - for(var = 0; var < old_num_binary_vars; var++) - new_num_binary_vars += (paired[var] == FALSE); - new_num_vars = new_num_binary_vars + pair->cnt; - new_num_vars += old_num_vars - old_num_binary_vars; - new_part_size = ALLOC(int, new_num_vars); - for(var = 0; var < pair->cnt; var++) - new_part_size[new_num_binary_vars + var] = 4; - for(var = 0; var < old_num_vars - old_num_binary_vars; var++) - new_part_size[new_num_binary_vars + pair->cnt + var] = - cube.part_size[old_num_binary_vars + var]; - setdown_cube(); - FREE(cube.part_size); - cube.num_vars = new_num_vars; - cube.num_binary_vars = new_num_binary_vars; - cube.part_size = new_part_size; - cube_setup(); - - /* hack with the labels to get them correct */ - if (adjust_labels) { - oldlabel = PLA->label; - PLA->label = ALLOC(char *, cube.size); - for(var = 0; var < pair->cnt; var++) { - newvar = cube.num_binary_vars*2 + var*4; - var1 = oldlabel[ (pair->var1[var]-1) * 2 + 1]; - var2 = oldlabel[ (pair->var2[var]-1) * 2 + 1]; - var1bar = oldlabel[ (pair->var1[var]-1) * 2]; - var2bar = oldlabel[ (pair->var2[var]-1) * 2]; - (void) sprintf(scratch, "%s+%s", var1bar, var2bar); - PLA->label[newvar] = util_strsav(scratch); - (void) sprintf(scratch, "%s+%s", var1bar, var2); - PLA->label[newvar+1] = util_strsav(scratch); - (void) sprintf(scratch, "%s+%s", var1, var2bar); - PLA->label[newvar+2] = util_strsav(scratch); - (void) sprintf(scratch, "%s+%s", var1, var2); - PLA->label[newvar+3] = util_strsav(scratch); - } - /* Copy the old labels for the unpaired binary vars */ - i = 0; - for(var = 0; var < old_num_binary_vars; var++) { - if (paired[var] == FALSE) { - PLA->label[2*i] = oldlabel[2*var]; - PLA->label[2*i+1] = oldlabel[2*var+1]; - oldlabel[2*var] = oldlabel[2*var+1] = (char *) NULL; - i++; - } - } - /* Copy the old labels for the remaining unpaired vars */ - new_mv_start = cube.num_binary_vars*2 + pair->cnt*4; - for(i = old_mv_start; i < old_size; i++) { - PLA->label[new_mv_start + i - old_mv_start] = oldlabel[i]; - oldlabel[i] = (char *) NULL; - } - /* free remaining entries in oldlabel */ - for(i = 0; i < old_size; i++) - if (oldlabel[i] != (char *) NULL) - FREE(oldlabel[i]); - FREE(oldlabel); - } - - /* the paired variables should not be sparse (cf. mv_reduce/raise_in)*/ - for(var = 0; var < pair->cnt; var++) - cube.sparse[cube.num_binary_vars + var] = 0; - FREE(paired); -} - -pcover pairvar(A, pair) -pcover A; -ppair pair; -{ - register pcube last, p; - register int val, p1, p2, b1, b0; - int insert_col, pairnum; - - insert_col = cube.first_part[cube.num_vars - 1]; - - /* stretch the cover matrix to make room for the paired variables */ - A = sf_delcol(A, insert_col, -4*pair->cnt); - - /* compute the paired values */ - foreach_set(A, last, p) { - for(pairnum = 0; pairnum < pair->cnt; pairnum++) { - p1 = cube.first_part[pair->var1[pairnum] - 1]; - p2 = cube.first_part[pair->var2[pairnum] - 1]; - b1 = is_in_set(p, p2+1); - b0 = is_in_set(p, p2); - val = insert_col + pairnum * 4; - if (/* a0 */ is_in_set(p, p1)) { - if (b0) - set_insert(p, val + 3); - if (b1) - set_insert(p, val + 2); - } - if (/* a1 */ is_in_set(p, p1+1)) { - if (b0) - set_insert(p, val + 1); - if (b1) - set_insert(p, val); - } - } - } - return A; -} - - -/* delvar -- delete variables from A, minimize the number of column shifts */ -pcover delvar(A, paired) -pcover A; -bool paired[]; -{ - bool run; - int first_run, run_length, var, offset = 0; - - run = FALSE; run_length = 0; - for(var = 0; var < cube.num_binary_vars; var++) - if (paired[var]) - if (run) - run_length += cube.part_size[var]; - else { - run = TRUE; - first_run = cube.first_part[var]; - run_length = cube.part_size[var]; - } - else - if (run) { - A = sf_delcol(A, first_run-offset, run_length); - run = FALSE; - offset += run_length; - } - if (run) - A = sf_delcol(A, first_run-offset, run_length); - return A; -} - -/* - find_optimal_pairing -- find which binary variables should be paired - to maximally reduce the number of terms - - This is essentially the technique outlined by T. Sasao in the - Trans. on Comp., Oct 1984. We estimate the cost of pairing each - pair individually using 1 of 4 strategies: (1) algebraic division - of F by the pair (exactly T. Sasao technique); (2) strong division - of F by the paired variables (using REDUCE/EXPAND/ IRREDUNDANT from - espresso); (3) full minimization using espresso; (4) exact - minimization. These are in order of both increasing accuracy and - increasing difficulty (!) - - Once the n squared pairs have been evaluated, T. Sasao proposes a - graph covering of nodes by disjoint edges. For now, I solve this - problem exhaustively (complexity = (n-1)*(n-3)*...*3*1 for n - variables when n is even). Note that solving this problem exactly - is the same as evaluating the cost function for all possible - pairings. - - n pairs - - 1, 2 1 - 3, 4 3 - 5, 6 15 - 7, 8 105 - 9,10 945 - 11,12 10,395 - 13,14 135,135 - 15,16 2,027,025 - 17,18 34,459,425 - 19,20 654,729,075 -*/ -void find_optimal_pairing(PLA, strategy) -pPLA PLA; -int strategy; -{ - int i, j, **cost_array; - - cost_array = find_pairing_cost(PLA, strategy); - - if (summary) { - printf(" "); - for(i = 0; i < cube.num_binary_vars; i++) - printf("%3d ", i+1); - printf("\n"); - for(i = 0; i < cube.num_binary_vars; i++) { - printf("%3d ", i+1); - for(j = 0; j < cube.num_binary_vars; j++) - printf("%3d ", cost_array[i][j]); - printf("\n"); - } - } - - if (cube.num_binary_vars <= 14) { - PLA->pair = pair_best_cost(cost_array); - } else { - (void) greedy_best_cost(cost_array, &(PLA->pair)); - } - printf("# "); - print_pair(PLA->pair); - - for(i = 0; i < cube.num_binary_vars; i++) - FREE(cost_array[i]); - FREE(cost_array); - - set_pair(PLA); - EXEC_S(PLA->F=espresso(PLA->F,PLA->D,PLA->R),"ESPRESSO ",PLA->F); -} - -int **find_pairing_cost(PLA, strategy) -pPLA PLA; -int strategy; -{ - int var1, var2, **cost_array; - int i, j, xnum_binary_vars, xnum_vars, *xpart_size, cost; - pcover T, Fsave, Dsave, Rsave; - pset mask; -/* char *s;*/ - - /* data is returned in the cost array */ - cost_array = ALLOC(int *, cube.num_binary_vars); - for(i = 0; i < cube.num_binary_vars; i++) - cost_array[i] = ALLOC(int, cube.num_binary_vars); - for(i = 0; i < cube.num_binary_vars; i++) - for(j = 0; j < cube.num_binary_vars; j++) - cost_array[i][j] = 0; - - /* Setup the pair structure for pairing variables together */ - PLA->pair = pair_new(1); - PLA->pair->cnt = 1; - - for(var1 = 0; var1 < cube.num_binary_vars-1; var1++) { - for(var2 = var1+1; var2 < cube.num_binary_vars; var2++) { - /* if anything but simple strategy, perform setup */ - if (strategy > 0) { - /* save the original covers */ - Fsave = sf_save(PLA->F); - Dsave = sf_save(PLA->D); - Rsave = sf_save(PLA->R); - - /* save the original cube structure */ - xnum_binary_vars = cube.num_binary_vars; - xnum_vars = cube.num_vars; - xpart_size = ALLOC(int, cube.num_vars); - for(i = 0; i < cube.num_vars; i++) - xpart_size[i] = cube.part_size[i]; - - /* pair two variables together */ - PLA->pair->var1[0] = var1 + 1; - PLA->pair->var2[0] = var2 + 1; - set_pair1(PLA, /* adjust_labels */ FALSE); - } - - - /* decide how to best estimate worth of this pairing */ - switch(strategy) { - case 3: - /*s = "exact minimization";*/ - PLA->F = minimize_exact(PLA->F, PLA->D, PLA->R, 1); - cost = Fsave->count - PLA->F->count; - break; - case 2: - /*s = "full minimization";*/ - PLA->F = espresso(PLA->F, PLA->D, PLA->R); - cost = Fsave->count - PLA->F->count; - break; - case 1: - /*s = "strong division";*/ - PLA->F = reduce(PLA->F, PLA->D); - PLA->F = expand(PLA->F, PLA->R, FALSE); - PLA->F = irredundant(PLA->F, PLA->D); - cost = Fsave->count - PLA->F->count; - break; - case 0: - /*s = "weak division";*/ - mask = new_cube(); - set_or(mask, cube.var_mask[var1], cube.var_mask[var2]); - T = dist_merge(sf_save(PLA->F), mask); - cost = PLA->F->count - T->count; - sf_free(T); - set_free(mask); - } - - cost_array[var1][var2] = cost; - - if (strategy > 0) { - /* restore the original cube structure -- free the new ones */ - setdown_cube(); - FREE(cube.part_size); - cube.num_binary_vars = xnum_binary_vars; - cube.num_vars = xnum_vars; - cube.part_size = xpart_size; - cube_setup(); - - /* restore the original cover(s) -- free the new ones */ - sf_free(PLA->F); - sf_free(PLA->D); - sf_free(PLA->R); - PLA->F = Fsave; - PLA->D = Dsave; - PLA->R = Rsave; - } - } - } - - pair_free(PLA->pair); - PLA->pair = NULL; - return cost_array; -} - -static int best_cost; -static int **cost_array; -static ppair best_pair; -static pset best_phase; -static pPLA global_PLA; -static pcover best_F, best_D, best_R; -static int pair_minim_strategy; - - -print_pair(pair) -ppair pair; -{ - int i; - - printf("pair is"); - for(i = 0; i < pair->cnt; i++) - printf (" (%d %d)", pair->var1[i], pair->var2[i]); - printf("\n"); -} - - -int greedy_best_cost(cost_array_local, pair_p) -int **cost_array_local; -ppair *pair_p; -{ - int i, j, besti, bestj, maxcost, total_cost; - pset cand; - ppair pair; - - pair = pair_new(cube.num_binary_vars); - cand = set_full(cube.num_binary_vars); - total_cost = 0; - - while (set_ord(cand) >= 2) { - maxcost = -1; - for(i = 0; i < cube.num_binary_vars; i++) { - if (is_in_set(cand, i)) { - for(j = i+1; j < cube.num_binary_vars; j++) { - if (is_in_set(cand, j)) { - if (cost_array_local[i][j] > maxcost) { - maxcost = cost_array_local[i][j]; - besti = i; - bestj = j; - } - } - } - } - } - pair->var1[pair->cnt] = besti+1; - pair->var2[pair->cnt] = bestj+1; - pair->cnt++; - set_remove(cand, besti); - set_remove(cand, bestj); - total_cost += maxcost; - } - set_free(cand); - *pair_p = pair; - return total_cost; -} - - -ppair pair_best_cost(cost_array_local) -int **cost_array_local; -{ - ppair pair; - pset candidate; - - best_cost = -1; - best_pair = NULL; - cost_array = cost_array_local; - - pair = pair_new(cube.num_binary_vars); - candidate = set_full(cube.num_binary_vars); - generate_all_pairs(pair, cube.num_binary_vars, candidate, find_best_cost); - pair_free(pair); - set_free(candidate); - return best_pair; -} - - -int find_best_cost(pair) -register ppair pair; -{ - register int i, cost; - - cost = 0; - for(i = 0; i < pair->cnt; i++) - cost += cost_array[pair->var1[i]-1][pair->var2[i]-1]; - if (cost > best_cost) { - best_cost = cost; - best_pair = pair_save(pair, pair->cnt); - } - if ((debug & MINCOV) && trace) { - printf("cost is %d ", cost); - print_pair(pair); - } -} - -/* - pair_all: brute-force approach to try all possible pairings - - pair_strategy is: - 2) for espresso - 3) for minimize_exact - 4) for phase assignment -*/ - -pair_all(PLA, pair_strategy) -pPLA PLA; -int pair_strategy; -{ - ppair pair; - pset candidate; - - global_PLA = PLA; - pair_minim_strategy = pair_strategy; - best_cost = PLA->F->count + 1; - best_pair = NULL; - best_phase = NULL; - best_F = best_D = best_R = NULL; - pair = pair_new(cube.num_binary_vars); - candidate = set_fill(set_new(cube.num_binary_vars), cube.num_binary_vars); - - generate_all_pairs(pair, cube.num_binary_vars, candidate, minimize_pair); - - pair_free(pair); - set_free(candidate); - - PLA->pair = best_pair; - PLA->phase = best_phase; -/* not really necessary - if (phase != NULL) - (void) set_phase(PLA->phase); -*/ - set_pair(PLA); - printf("# "); - print_pair(PLA->pair); - - sf_free(PLA->F); - sf_free(PLA->D); - sf_free(PLA->R); - PLA->F = best_F; - PLA->D = best_D; - PLA->R = best_R; -} - - -/* - * minimize_pair -- called as each pair is generated - */ -int minimize_pair(pair) -ppair pair; -{ - pcover Fsave, Dsave, Rsave; - int i, xnum_binary_vars, xnum_vars, *xpart_size; - - /* save the original covers */ - Fsave = sf_save(global_PLA->F); - Dsave = sf_save(global_PLA->D); - Rsave = sf_save(global_PLA->R); - - /* save the original cube structure */ - xnum_binary_vars = cube.num_binary_vars; - xnum_vars = cube.num_vars; - xpart_size = ALLOC(int, cube.num_vars); - for(i = 0; i < cube.num_vars; i++) - xpart_size[i] = cube.part_size[i]; - - /* setup the paired variables */ - global_PLA->pair = pair; - set_pair1(global_PLA, /* adjust_labels */ FALSE); - - /* call the minimizer */ - if (summary) - print_pair(pair); - switch(pair_minim_strategy) { - case 2: - EXEC_S(phase_assignment(global_PLA,0), "OPO ", global_PLA->F); - if (summary) - printf("# phase is %s\n", pc1(global_PLA->phase)); - break; - case 1: - EXEC_S(global_PLA->F = minimize_exact(global_PLA->F, global_PLA->D, - global_PLA->R, 1), "EXACT ", global_PLA->F); - break; - case 0: - EXEC_S(global_PLA->F = espresso(global_PLA->F, global_PLA->D, - global_PLA->R), "ESPRESSO ", global_PLA->F); - break; - default: - break; - } - - /* see if we have a new best solution */ - if (global_PLA->F->count < best_cost) { - best_cost = global_PLA->F->count; - best_pair = pair_save(pair, pair->cnt); - best_phase = global_PLA->phase!=NULL?set_save(global_PLA->phase):NULL; - if (best_F != NULL) sf_free(best_F); - if (best_D != NULL) sf_free(best_D); - if (best_R != NULL) sf_free(best_R); - best_F = sf_save(global_PLA->F); - best_D = sf_save(global_PLA->D); - best_R = sf_save(global_PLA->R); - } - - /* restore the original cube structure -- free the new ones */ - setdown_cube(); - FREE(cube.part_size); - cube.num_binary_vars = xnum_binary_vars; - cube.num_vars = xnum_vars; - cube.part_size = xpart_size; - cube_setup(); - - /* restore the original cover(s) -- free the new ones */ - sf_free(global_PLA->F); - sf_free(global_PLA->D); - sf_free(global_PLA->R); - global_PLA->F = Fsave; - global_PLA->D = Dsave; - global_PLA->R = Rsave; - global_PLA->pair = NULL; - global_PLA->phase = NULL; -} - -generate_all_pairs(pair, n, candidate, action) -ppair pair; -int n; -pset candidate; -int (*action)(); -{ - int i, j; - pset recur_candidate; - ppair recur_pair; - - if (set_ord(candidate) < 2) { - (*action)(pair); - return; - } - - recur_pair = pair_save(pair, n); - recur_candidate = set_save(candidate); - - /* Find first variable still in the candidate set */ - for(i = 0; i < n; i++) - if (is_in_set(candidate, i)) - break; - - /* Try all pairs of i with other variables */ - for(j = i+1; j < n; j++) - if (is_in_set(candidate, j)) { - /* pair (i j) -- remove from candidate set for future pairings */ - set_remove(recur_candidate, i); - set_remove(recur_candidate, j); - - /* add to the pair array */ - recur_pair->var1[recur_pair->cnt] = i+1; - recur_pair->var2[recur_pair->cnt] = j+1; - recur_pair->cnt++; - - /* recur looking for the end ... */ - generate_all_pairs(recur_pair, n, recur_candidate, action); - - /* now break this pair, and restore candidate set */ - recur_pair->cnt--; - set_insert(recur_candidate, i); - set_insert(recur_candidate, j); - } - - /* if odd, generate all pairs which do NOT include i */ - if ((set_ord(candidate) % 2) == 1) { - set_remove(recur_candidate, i); - generate_all_pairs(recur_pair, n, recur_candidate, action); - } - - pair_free(recur_pair); - set_free(recur_candidate); -} - -ppair pair_new(n) -register int n; -{ - register ppair pair1; - - pair1 = ALLOC(pair_t, 1); - pair1->cnt = 0; - pair1->var1 = ALLOC(int, n); - pair1->var2 = ALLOC(int, n); - return pair1; -} - - -ppair pair_save(pair, n) -register ppair pair; -register int n; -{ - register int k; - register ppair pair1; - - pair1 = pair_new(n); - pair1->cnt = pair->cnt; - for(k = 0; k < pair->cnt; k++) { - pair1->var1[k] = pair->var1[k]; - pair1->var2[k] = pair->var2[k]; - } - return pair1; -} - - -int pair_free(pair) -register ppair pair; -{ - FREE(pair->var1); - FREE(pair->var2); - FREE(pair); -} |