if (pnr_var_mean > 0) {
        pnr_var_mean /= 1.0 * numVars;
    }
    if (horn_mean > 0) {
        horn_mean /= 1.0 * numVars;
    }

    vcg_var_spread = vcg_var_max - vcg_var_min;
    pnr_var_spread = pnr_var_max - pnr_var_min;
    horn_spread = horn_max - horn_min;

    auto func2 = [&](unsigned size, unsigned pos_vars, unsigned) -> void {
        if ( size == 0 ) {
            return;
        }

        double _size = (double)size / (1.0 * numVars);
        vcg_cls_std += (vcg_cls_mean - _size) * (vcg_cls_mean - _size);

        double _pnr = 0.5 + ((2.0 * (double)pos_vars - (double)size) / (2.0 * (double)size));
        pnr_cls_std += (pnr_cls_mean - _pnr) * (pnr_cls_mean - _pnr);
    };
    for_all_clauses(func2, empty_func);

    if ( vcg_cls_std > eps && vcg_cls_mean > eps ) {
        vcg_cls_std = sqrt(vcg_cls_std / (1.0 * numClauses)) / vcg_cls_mean;
    } else {
        vcg_cls_std = 0;
    }

    if ( pnr_cls_std > eps && vcg_cls_mean > eps ) {
        pnr_cls_std = sqrt(pnr_cls_std / (1.0 * numClauses)) / pnr_cls_mean;
    } else {
        pnr_cls_std = 0;
    }

    for ( int vv = 0; vv < (int)myVars.size(); vv++ ) {
        if ( myVars[vv].size == 0 ) {
            continue;
        }

        double _size = myVars[vv].size / (1.0 * numClauses);
        vcg_var_std += (vcg_var_mean - _size) * (vcg_var_mean - _size);

        double _pnr = 0.5 + ((2.0 * myVars[vv].numPos - myVars[vv].size) / (2.0 * myVars[vv].size));
        pnr_var_std += (pnr_var_mean - _pnr) * (pnr_var_mean - _pnr);

        double _horn = myVars[vv].horn / (1.0 * numClauses);
        horn_std += (horn_mean - _horn) * (horn_mean - _horn);
    }
    if ( vcg_var_std > eps && vcg_var_mean > eps ) {
        vcg_var_std = sqrt(vcg_var_std / (1.0 * numVars)) / vcg_var_mean;
    } else {
        vcg_var_std = 0;
    }

    if ( pnr_var_std > eps && pnr_var_mean > eps ) {