src/misc/espresso/pair.c File Reference

#include "espresso.h"

Include dependency graph for pair.c:

Go to the source code of this file.

Functions
void	set_pair (pPLA PLA)
void	set_pair1 (pPLA PLA, bool adjust_labels)
pcover	pairvar (pcover A, ppair pair)
pcover	delvar (pcover A, paired)
void	find_optimal_pairing (pPLA PLA, int strategy)
int **	find_pairing_cost (pPLA PLA, int strategy)
	print_pair (ppair pair)
int	greedy_best_cost (int **cost_array_local, ppair *pair_p)
ppair	pair_best_cost (int **cost_array_local)
int	find_best_cost (ppair pair)
	pair_all (pPLA PLA, int pair_strategy)
int	minimize_pair (ppair pair)
	generate_all_pairs (ppair pair, int n, pset candidate, int(*action)())
ppair	pair_new (int n)
ppair	pair_save (ppair pair, int n)
int	pair_free (ppair pair)
Variables
static int	best_cost
static int **	cost_array
static ppair	best_pair
static pset	best_phase
static pPLA	global_PLA
static pcover	best_F
static pcover	best_D
static pcover	best_R
static int	pair_minim_strategy

---

Function Documentation

pcover delvar	(	pcover	A,
		paired
	)

Definition at line 161 of file pair.c.

{
    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;
}

int find_best_cost

(

ppair

pair

)

Definition at line 440 of file pair.c.

{
    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);
    }
}

void find_optimal_pairing	(	pPLA	PLA,
		int	strategy
	)

Definition at line 222 of file pair.c.

{
    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	(	pPLA	PLA,
		int	strategy
	)

Definition at line 259 of file pair.c.

{
    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;
}

generate_all_pairs	(	ppair	pair,
		int	n,
		pset	candidate,
		int (*)()	action
	)

Definition at line 585 of file pair.c.

{
    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);
}

int greedy_best_cost	(	int **	cost_array_local,
		ppair *	pair_p
	)

Definition at line 381 of file pair.c.

{
    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;
}

int minimize_pair

(

ppair

pair

)

Definition at line 510 of file pair.c.

{
    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;
}

pair_all	(	pPLA	PLA,
		int	pair_strategy
	)

Definition at line 467 of file pair.c.

{
    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;
}

ppair pair_best_cost

(

int **

cost_array_local

)

Definition at line 421 of file pair.c.

{
    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 pair_free

(

ppair

pair

)

Definition at line 669 of file pair.c.

{
    FREE(pair->var1);
    FREE(pair->var2);
    FREE(pair);
}

ppair pair_new

(

int

n

)

Definition at line 639 of file pair.c.

{
    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	(	ppair	pair,
		int	n
	)

Definition at line 652 of file pair.c.

{
    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;
}

pcover pairvar	(	pcover	A,
		ppair	pair
	)

Definition at line 121 of file pair.c.

{
    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;
}

print_pair

(

ppair

pair

)

Definition at line 369 of file pair.c.

{
    int i;

    printf("pair is");
    for(i = 0; i < pair->cnt; i++)
        printf (" (%d %d)", pair->var1[i], pair->var2[i]);
    printf("\n");
}

void set_pair

(

pPLA

PLA

)

Definition at line 12 of file pair.c.

{
    set_pair1(PLA, TRUE);
}

void set_pair1	(	pPLA	PLA,
		bool	adjust_labels
	)

Definition at line 18 of file pair.c.

{
    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);
}

---

Variable Documentation

int best_cost [static]

Definition at line 360 of file pair.c.

pcover best_D [static]

Definition at line 365 of file pair.c.

pcover best_F [static]

Definition at line 365 of file pair.c.

ppair best_pair [static]

Definition at line 362 of file pair.c.

pset best_phase [static]

Definition at line 363 of file pair.c.

pcover best_R [static]

Definition at line 365 of file pair.c.

int** cost_array [static]

Definition at line 361 of file pair.c.

pPLA global_PLA [static]

Definition at line 364 of file pair.c.

int pair_minim_strategy [static]

Definition at line 366 of file pair.c.