private void elim() {
        final long steps = this.limits.simpSteps;
        assert this.level == 0;
        assert !this.config.plain;
        if (!this.config.elim) { return; }
        assert this.simplifier == Simplifier.TOPSIMP;
        this.simplifier = Simplifier.ELIM;
        updateCands();
        final long limit;
        if (this.stats.simplifications <= this.config.elmrtc) { limit = Long.MAX_VALUE; } else {
            limit = this.stats.steps + 10 * steps / sizePenalty();
        }
        while (this.empty == null && !this.candsElim.empty() && this.stats.steps++ < limit) {
            final int cand = this.candsElim.top();
            final long priority = this.candsElim.priority(cand);
            this.candsElim.pop(cand);
            if (priority == 0 || !var(cand).free() || donotelim(cand)) { continue; }
            backward(cand);
            backward(-cand);
            if (tryElim(cand)) { doElim(cand); }
        }
        assert this.schedule;
        this.schedule = false;
        assert this.simplifier == Simplifier.ELIM;
        this.simplifier = Simplifier.TOPSIMP;
        dumpEliminatedRedundant();
    }
private void elim ( ) { final long steps = this . limits . simpSteps ; assert this . level == 0 ; assert ! this . config . plain ; if ( ! this . config . elim ) { return ; } assert this . simplifier == Simplifier . TOPSIMP ; this . simplifier = Simplifier . ELIM ; updateCands ( ) ; final long limit ; if ( this . stats . simplifications <= this . config . elmrtc ) { limit = Long . MAX_VALUE ; } else { limit = this . stats . steps + 10 * steps / sizePenalty ( ) ; } while ( this . empty == null && ! this . candsElim . empty ( ) && this . stats . steps ++ < limit ) { final int cand = this . candsElim . top ( ) ; final long priority = this . candsElim . priority ( cand ) ; this . candsElim . pop ( cand ) ; if ( priority == 0 || ! var ( cand ) . free ( ) || donotelim ( cand ) ) { continue ; } backward ( cand ) ; backward ( - cand ) ; if ( tryElim ( cand ) ) { doElim ( cand ) ; } } assert this . schedule ; this . schedule = false ; assert this . simplifier == Simplifier . ELIM ; this . simplifier = Simplifier . TOPSIMP ; dumpEliminatedRedundant ( ) ; }
(Bounded) Variable Elimination = (B)VE = Clause Distribution = DP.
<p>
This is the same bounded variable elimination technique as in the SatElite paper except that it performs
subsumption and self-subsuming resolution on-the-fly while trying to eliminate a candidate variable.  It is also
limited by the number of resolution steps.