// poor man's MaxSMT
// if we minimize, first try false, then true
// if we maximize, do contrariwise
bool run_poor_mans_MaxSMT(struct ctx* ctx)
{
    if (verbose>0)
        printf ("%s() begin\n", __FUNCTION__);
    assert (ctx->maxsat==true);
    struct PicoSAT *p=picosat_init ();

    add_clauses_to_picosat(ctx, p);

    if (ctx->write_CNF_file)
    {
        write_CNF(ctx, "tmp.cnf");
        printf ("CNF file written to tmp.cnf\n");
    };

    int array[ctx->min_max_var->width];
    int res;
    // do this starting at the MSB moving towards the LSB:
    for (int idx=ctx->min_max_var->width-1; idx>=0; idx--)
    {
        // try the first false/true
        array[idx]=ctx->min_or_max==false ? 0 : 1;
        if (verbose>0)
            printf ("idx=%d trying %s\n", idx, ctx->min_or_max==false ? "false" : "true");
        picosat_assume (p, (ctx->min_or_max==false ? -1 : 1) * (ctx->min_max_var->SAT_var+idx));

        res=picosat_sat (p,-1);
        if (res==10)
        {
            if (verbose>0)
                printf ("got SAT\n");
            if (idx!=0)
            {
                // add a newly discovered correct bit as a clause
                // but do this only if this is not the last bit
                // if the bit is the last/lowest (idx==0), we want to prevent PicoSAT to be switched out of SAT state
                // (PicoSAT do this after picosat_add() call)
                // because we are fetching result sooner afterwards
                picosat_add (p, (ctx->min_or_max==false ? -1 : 1) * (ctx->min_max_var->SAT_var+idx));
                picosat_add (p, 0);
            }
            // proceed to the next bit:
            continue;
        };
        if (verbose>0)
            printf ("got UNSAT\n");
        assert (res==20); // must be in UNSAT state

        // try the second false/true
        array[idx]=ctx->min_or_max==false ? 1 : 0;
        if (verbose>0)
            printf ("idx=%d trying %s\n", idx, ctx->min_or_max==false ? "true" : "false");
        picosat_assume (p, (ctx->min_or_max==false ? 1 : -1) * (ctx->min_max_var->SAT_var+idx));

        res=picosat_sat (p,-1);
        if (res==10)
        {
            if (verbose>0)
                printf ("got SAT\n");
            if (idx!=0)
            {
                picosat_add (p, (ctx->min_or_max==false ? 1 : -1) * (ctx->min_max_var->SAT_var+idx));
                picosat_add (p, 0);
            };
        }
        else if (res==20)
        {
            if (verbose>0)
            {
                printf ("got UNSAT\n");
                printf ("%s() begin -> false\n", __FUNCTION__);
            };
            // UNSAT for both false and true for this bit at idx, return UNSAT for this instance:
            return false;
        }
        else
        {
            assert(0);
        };
    };
    // must have a solution at this point
    fill_variables_from_picosat(ctx, p);
    // construct a value from array[]:
    ctx->min_max_var->val=SAT_solution_to_value(array, ctx->min_max_var->width);
    if (verbose>0)
        printf ("%s() begin -> true, val=%llu\n", __FUNCTION__, ctx->min_max_var->val);
    return true;
};