bin_mincov.c

主要进行大规模的电路综合

{
    int i, row, neg_unate, pos_unate;
    sm_row *prow;
    sm_element *elem;
    sm_matrix *result;
    value_t * row_value;

    /* reorder rows; longest first */
    /* row_value[i].elem->row_num gives the number of the old row in the i-th 
     * position of the new matrix;
     */
    result = sm_alloc ();
    if (M->last_row == NIL(sm_row) || M->last_col == NIL(sm_col)) {
		return result;
	}
    row_value = ALLOC (value_t, M->nrows);
    i = 0;
    sm_foreach_row (M, prow) {
        if (prow->length) {
            row_value[i].elem = prow->first_col;
            if (g_option & 1) {
                /* save original order for ties */
                row_value[i].value = 10000 * prow->length + i;
            }
            else if (g_option & 256) {
            /* define as value the sum of all column values */
                row_value[i].value = 0;
                sm_foreach_row_element (prow, elem) {
                    row_value[i].value += WEIGHT (weights, elem->col_num);
                }
            }
            else {
                row_value[i].value = prow->length;
            }

            if (g_option & (512 | 1024)) {
            /* check if it is 'unate' */
                pos_unate = 1;
                neg_unate = 1;
                sm_foreach_row_element (prow, elem) {
                    if (elem->col_num % 2) {
                        pos_unate = 0;
                    }
                    else {
                        neg_unate = 0;
                    }
                }

                if (pos_unate || neg_unate) {
                    if (g_option & 512) {
                        /* 'unate' rows first */
                        row_value[i].value += 10000;
                    }
                    else {
                        /* 'unate' rows last */
                        row_value[i].value -= 10000;
                    }
                }
            }

            i++;
        }
    }

    if (g_option & 2) {
        /* do not sort rows */
    }
    else if (g_option & 4096) {
        qsort ((char *) row_value, M->nrows, sizeof(value_t), compare_rev);
    }
    else {
        qsort ((char *) row_value, M->nrows, sizeof(value_t), compare);
    }

    /* permute the rows of M into A, according to col_value */
    sm_resize(result, M->last_row->row_num, M->last_col->col_num);
    for (i = 0; i < M->nrows; i++) {
        /* the i-th old column has row_value[i].elem->row_num now !! */
        prow = sm_get_row (M, row_value[i].elem->row_num);
        sm_foreach_row_element (prow, elem) {
            (void) sm_insert (result, i, elem->col_num);
        }
    }

    if (g_debug > 2) {
        (void) fprintf (misout, "Partial row ordering:\n");
        for (row = 0; row < result->nrows; row++) {
            (void) fprintf (misout, "%d ", row_value[row].elem->row_num);
        }
        (void) fprintf (misout, "\n");
    }

    FREE (row_value);

    return result;
}

/* Apply Mathony's algorithm to generate all weighted primes of matrix A.
 * 1) if we reached the end of the recursion, check if the current solution
 *    improves the best seen so far, and save it.
 * 2) rule 3: if the current solution contains a literal appearing also
 *    in the current row, ignore the current row.
 * 3) for each literal in the current row (sum):
 *    a) rule 1: if the current solution contains the complement of the 
 *       literal, ignore the current literal;
 *    b) rule 5: if the current solution plus the cost of the current literal
 *       would cost more than the best solution, ignore the current literal;
 *    c) rule 2: if a row at an upper level contains the same literal yet to
 *       be expanded, ignore the current literal and mark the literal in the
 *       upper row;
 *    d) rule 4: if a row at an upper level contains the same literal already
 *       expanded and if rule 2 was not applied with respect to the literal
 *       in the upper row in the current expansion (i.e. it is not marked),
 *       ignore the current literal;
 *    e) otherwise, add the current literal to the solution and recur for the
 *       next row.
 * 4) remove rule 2 marks from the current rows (if any).
 */

void
sm_bin_mincov (row_num)

int row_num;

{
    sm_row *curr_row;
    sm_element *elem, *uplevel_elem;
    int literal, literal_bar, col;

    call_count++;
#ifdef DEBUG
    /* debugging; dbx is too slow... */
    if (call_count == cc) {
        (void) fprintf (miserr, "got it\n");
    }
#endif

    /* check for recursion end, and record the solution if improving */
    if (row_num == A->nrows) {
        if (g_record_fun) {
            curr_row = sm_row_alloc();
            for (col = 0; col < A->last_col->col_num + 1; col++) {
                if (is_in_set (sol->set, col)) {
                    sm_row_insert (curr_row, col);
                }
            }
            if ((*g_record_fun) (curr_row)) {
                ended = 1;
            }
            sm_row_free (curr_row);
            return;
        }
        else if (sol->cost < best->cost) {
            got_best = 1;
            bin_solution_free (best);
            best = bin_solution_dup (sol, A->last_col->col_num + 1);

            if (g_debug > 0) {
                (void) fprintf(misout, "  new 'best' solution %d; time %s; calls %d\n", 
                    best->cost,
                    util_print_time(util_cpu_time() - start_time),
                    call_count);
                (void) fflush (misout);
#ifdef DEBUG
                if (g_debug > 5) {
                    if (g_debug > 9) {
                        sp (best->set);
                    }
                    else {
                        (void) fprintf (misout, "\n");
                    }
                }
#endif
            }

        }
        leaves_count++;
        if (g_heu) {
            ended = 1;
        }
        return;
    }

    /* initialize the level */
    curr_row = sm_get_row (A, row_num);
    expanded[row_num] = NIL(sm_element);    /* nothing chosen... */

#ifdef DEBUG
    if (g_debug > 9) {
        print_lev (row_num, "beginning ");
        rp (curr_row);
    }
#endif

    /* begin R3 */
    /* check if any of the literals in the row appears in the solution already;
     * if so ignore the current row
     */
    sm_foreach_row_element (curr_row, elem) {
        if (is_in_set ((sol->set), elem->col_num)) {
#ifdef DEBUG
            if (g_debug > 9) {
                print_lev (row_num, "ignoring (R3)\n");
            }
#endif

            r3++;
            /* recur for next row */
            sm_bin_mincov (row_num + 1);
            return;
        }
    }
    /* end R3 */

    /* now select each literal in turn */
    for (col = 0; ! ended && col < curr_row->length; col++) {
        elem = order[row_num][col];

        literal = elem->col_num;
        if (! is_unate) {
            literal_bar = GETBAR (literal);

            /* begin R1 */
            /* check if literal appears complemented in the solution; if so
             * ignore the literal
             */
            if (is_in_set ((sol->set), literal_bar)) {
#ifdef DEBUG
                if (g_debug > 9) {
                    print_lev (row_num, "pruning (R1) %s\n", 
                        literal_name (literal));
                }
#endif

                r1++;
                continue;
            }
            /* end R1 */
        }

        /* begin R5 */
        /* check if adding the current literal would make the solution worse;
         * if so, ignore the literal
         */
        if (sol->cost + WEIGHT(weights, literal) >= best->cost) {
#ifdef DEBUG
            if (g_debug > 6) {
                print_lev (row_num, "pruning (R5) (cost=%d) ", 
                    sol->cost + WEIGHT(weights, literal));
                if (g_debug > 9) {
                    (void) fprintf (misout, "%s ", literal_name (literal));
                    sp (sol->set);
                }
                else {
                    (void) fprintf (misout, "\n");
                }
            }
#endif

            r5++;
            continue;
        }
        /* end R5 */

        /* begin R2 and R4 */
        /* prepare for rule 5 and 6 check:
         * update the uplevel_elem pointer to be the first element in the 
         * same column (if any) with row < row_num (i.e. belonging to
         * an upper sum) and with expanded[row] != 0.
         * If this element was EXPANDED, then the currently expanded element
         * at that level must not have been MARKED
         */
        for (uplevel_elem = elem->prev_row; uplevel_elem != NIL(sm_element);
            uplevel_elem = uplevel_elem->prev_row) {
            if (expanded[uplevel_elem->row_num]) {
                if ((EXPANDED & (sm_get (int, uplevel_elem)))) {
                    if (! (MARKED & 
                        (sm_get (int, expanded[uplevel_elem->row_num])))) {
                        break;
                    }
                }
                else {
                    break;
                }
            }
        }

        /* check if the same literal appears at an upper level */
        if (uplevel_elem != NIL(sm_element)) {

            /* check if it was a yet unexpanded literal; if so, ignore the
             * current literal and record this, marking the current literal
             * at the upper level (and the row, for a faster reset).
             */
            if (! (EXPANDED & (sm_get (int, uplevel_elem)))) {
                sm_put (uplevel_elem, ((sm_get (int, uplevel_elem)) | MARKED));
#ifdef DEBUG
                if (g_debug > 9) {
                    print_lev (row_num, "pruning (R2) %s\n", 
                        literal_name (literal));
                }
#endif
                r2++;
                continue;
            }
            else {
            /* ignore the current literal (no need to record it...) */
#ifdef DEBUG
                if (g_debug > 9) {
                    print_lev (row_num, "pruning (R4) %s\n", 
                        literal_name (literal));
                }
#endif
                r4++;
                continue;
            }
        }
        /* end R2 and R4 */ 
        
        /* add the current literal to the solution and recur */
        expanded[row_num] = elem;
        sm_put (elem, ((sm_get (int, elem)) | EXPANDED));
        bin_solution_add (sol, weights, literal);

#ifdef DEBUG
        if (g_debug > 9) {
            print_lev (row_num, "choosing %s: ", literal_name (literal));
            sp (sol->set);
        }
#endif

        sm_bin_mincov (row_num + 1);

        /* remove the current literal */
        bin_solution_del (sol, weights, literal);
    }

    /* end of literal selection loop */

    /* un-mark the current row */
    sm_foreach_row_element (curr_row, elem) {
        sm_put (elem, 0);
    }

    expanded[row_num] = NIL(sm_element);

#ifdef DEBUG
    if (g_debug > 9) {
        print_lev (row_num, "ending\n");
    }
#endif
}

/* compare two value records
 */
static int 
compare (value1, value2)

value_t *value1, *value2;

{
    return value2->value - value1->value;
}

static int 
compare_rev (value1, value2)

value_t *value1, *value2;

{
    return value1->value - value2->value;
}

/* debugging stuff */
static char *
literal_name (literal)

int literal;

{
    static char buf[20];

    (void) sprintf (buf, "%d", literal);
    /* 
    if (! (literal % 2)) {
        (void) sprintf (buf, "%d", literal / 2);
    }
    else {
        (void) sprintf (buf, "%d'", literal / 2);
    } */
    return buf;
}

rp (row)

sm_row *row;

{
    sm_element *element;

    sm_foreach_row_element (row, element) {
        (void) fprintf (misout, "%s ", literal_name (element->col_num));
    }
    (void) fprintf (misout, "\n");
}

sp (set)
pset set;

{
    int i;

    for (i = 0; i < A->last_col->col_num + 1; i++) {
        if (is_in_set (set, i)) {
            (void) fprintf (misout, "%s ", literal_name (i));
        }
    }
    (void) fprintf (misout, "\n");
}

print_lev (row_num, p1, p2, p3, p4)

int row_num;
char *p1, *p2, *p3, *p4;

{
    int i;

    (void) fprintf (misout, "%d\t ", call_count);
    for (i = 0; i < row_num; i++) {
        putchar (' ');
        putchar (' ');
    }
    (void) fprintf (misout, p1, p2, p3, p4);
}

ps (set)
pset set;
{
    (void) fprintf (misout, ps1(set));
}

pm (mat)
sm_matrix *mat;
{
    sm_print (misout, mat);
}

wm (mat)
sm_matrix *mat;
{
    sm_write (misout, mat);
}

static int 
verify_cover(A, cover)
sm_matrix *A;
sm_row *cover;
{
    sm_row *prow;

    sm_foreach_row(A, prow) {
    if (! sm_row_intersects(prow, cover)) {
        return 0;
    }
    }
    return 1;
}