gistfile1.txt

int solve(formula* form)
{
    /* Create the structures to store the state of the
     * algorithm */
    bool *assigned = (bool *) calloc(form->nvars + 1, sizeof(bool));
    bool *vals = (bool *) calloc(form->nvars + 1, sizeof(bool));
    stack_item **sitems = (stack_item **) malloc(form->nvars * sizeof(stack_item*));

    stack s;
    s.items = sitems;
    s.top = -1;
    s.size = 0;

    literal *lp;
    literal *lp1;
    stack_item *sip;

    // Foreach clause in formula
    int i;
    for (i = 0; i < form->nclauses; i++)
    {
        // Get a pointer to the literal that needs assignment, if one exists
        if ((lp = is_unitclause(form->clauses[i], assigned, vals)) != NULL) {
            // COPY THE LITERAL POINTER
            //lp1 = (literal*) malloc(sizeof(literal));
            //memcpy(lp1, lp, sizeof(literal));

            assert_literal(lp, vals, assigned);
            stack_item si = {lp, i, 0};

            // COPY THE STACK ITEM
            sip = (stack_item*) malloc(sizeof(stack_item));
            memcpy(sip, &si, sizeof(stack_item));

            push_stack(&s, sip);
            if (DEBUG)
                print_stack(&s);
        }
        else {
            // If all literals are assigned
            if (alllits_assigned(form->clauses[i], assigned)) {
                // If clause satisfied
                if (!clause_satisfied(form->clauses[i], vals)) {
                    // "backtrack"
                    stack_item *item = pop_stack(&s);
                    if (DEBUG)
                        print_stack(&s);
                    if (item == NULL) {
                        return UNSATISFIABLE;
                    }
                    assigned[item->lp->id] = 0;

                    while (!item->guess) {
                        item = pop_stack(&s);
                        if (DEBUG)
                            print_stack(&s);
                        if (item == NULL) {
                            return UNSATISFIABLE;
                        }
                        assigned[item->lp->id] = 0;
                    }

                    // flip sign
                    item->lp->sign = !(item->lp->sign);
                    vals[item->lp->id] = !(vals[item->lp->id]);

                    // flip guess
                    item->guess = 0;
                    push_stack(&s, item);

                    assigned[item->lp->id] = 1;

                    if (DEBUG)
                        print_stack(&s);

                    // set the clause looping index
                    i = (item->ci) - 1;
                }
            }
            else {
                // Foreach literal
                int j;
                for(j = 0; j < form->clauses[i]->length; j++) {
                    // If clause is a unit clause:
                    if ((lp = is_unitclause(form->clauses[i], assigned, vals)) != NULL) {

                        // COPY THE LITERAL POINTER
                        //lp1 = (literal*) malloc(sizeof(literal));
                        //memcpy(lp1, lp, sizeof(literal));

                        assert_literal(lp, vals, assigned);
                        stack_item si = {lp, i, 0};

                        // COPY THE STACK ITEM
                        sip = (stack_item*) malloc(sizeof(stack_item));
                        memcpy(sip, &si, sizeof(stack_item));

                        push_stack(&s, sip);

                        if (DEBUG)
                            print_stack(&s);
                    }
                    else {
                        // Guess on literal if literal not assigned
                        lp = form->clauses[i]->lits[j];
                        int lit_id = lp->id;

                        // COPY THE LITERAL POINTER
                        lp1 = (literal*) malloc(sizeof(literal));
                        memcpy(lp1, lp, sizeof(literal));

                        if (!assigned[lit_id]) {
                            assert_literal(lp1, vals, assigned);
                            stack_item si = {lp1, i, 1};

                            // COPY THE STACK ITEM
                            sip = (stack_item*) malloc(sizeof(stack_item));
                            memcpy(sip, &si, sizeof(stack_item));

                            push_stack(&s, sip);
                            if (DEBUG)
                                print_stack(&s);
                        }
                    }
                }
            }
        }
    }

    // Perform cleanup before returning
    free(assigned);
    free(vals);

    // Cleanup any remaining items on the stack
    for(i = 0; i < s.size; i++) {
        free(s.items[i]);
    }

    // If we get this far the assumption is that we could satisfy the formula
    return SATISFIABLE;
}