First, what is incremental SAT? When a SAT-solver is "warmed up", and you want only to alter list of clauses slightly by adding one, why to reset it? In my toy SMT solver, I use incremental SAT for model counting, or getting all models: see picosat_get_all_models() function.
Also, many SAT solvers supports "assumptions". That is you supply a list of clauses + "temporary" clauses that will be dropped each time.
Now a digression: this is my own binary search implementation:
/* This is yet another explanation of binary search. However, it works only on array sizes = 2^n You know, like bank robbers in movies rotating a wheel on a safe (I don't know how it's called correctly) and find all digits consecutively. This is like brute-fource. We do here the same: we try 0/1 for each bit of index value. We start at 1, and if the array value at this index is too large, we clear the bit to 0 and proceed to the next (lower) bit. The array here has 32 numbers. The array index has 5 bits ( log2(32)==5 ). And you can clearly see that one need only 5 steps to find a value in an array of sorted numbers. The result: ========================================== testing idx=0x10 or 16 bit 4 is incorrect, it's 0, so we clear it testing idx=0x8 or 8 bit 3 is correct, it's 1 testing idx=0xc or 12 bit 2 is correct, it's 1 testing idx=0xe or 14 bit 1 is incorrect, it's 0, so we clear it testing idx=0xd or 13 found, idx=0xd or 13 ========================================== */ #include#include // array of sorted random numbers: int array[32]= { 335, 481, 668, 1169, 1288, 1437, 1485, 1523, 1839, 2058, 2537, 2585, 2698, 2722, 3245, 3675, 4067, 4139, 4356, 4599, 5578, 6334, 6751, 7244, 7845, 8220, 8272, 8296, 8297, 8358, 9138, 9650 }; void binsearch (int val_to_find) { int idx=0; for (int bit=4; ; bit--) { // set the bit: idx|=1<<bit; printf ("testing idx=0x%x or %d\n", idx, idx); if (array[idx]==val_to_find) { printf ("found, idx=0x%x or %d\n", idx, idx); exit(0); }; // array[idx] is too small? if (array[idx]<val_to_find) { // do nothing, the current bit correct, proceed to the next bit printf ("bit %d is correct, it's 1\n", bit); }; // array[idx] is too big? if (array[idx]>val_to_find) { // clear the current bit, because it's incorrect idx&=~(1<<bit); printf ("bit %d is incorrect, it's 0, so we clear it\n", bit); }; }; }; int main() { binsearch(2722); };
You wouldn't use it, but I wrote it because it's fits so nicely on SAT.
To solve an optimization problem, you want to find some "optimum" variable, that is minimized or maximized. Like in my implementation of binary search, I can try bit by bit, but these are added as assumptions.
// 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;
};
( https://github.com/DennisYurichev/MK85/blob/master/MK85.cc )
For the popscicle problem:
idx=15 trying true got UNSAT idx=15 trying false got SAT idx=14 trying true got UNSAT idx=14 trying false got SAT idx=13 trying true got UNSAT idx=13 trying false got SAT idx=12 trying true got UNSAT idx=12 trying false got SAT idx=11 trying true got UNSAT idx=11 trying false got SAT idx=10 trying true got UNSAT idx=10 trying false got SAT idx=9 trying true got UNSAT idx=9 trying false got SAT idx=8 trying true got UNSAT idx=8 trying false got SAT idx=7 trying true got UNSAT idx=7 trying false got SAT idx=6 trying true got UNSAT idx=6 trying false got SAT idx=5 trying true got UNSAT idx=5 trying false got SAT idx=4 trying true got UNSAT idx=4 trying false got SAT idx=3 trying true got SAT idx=2 trying true got SAT idx=1 trying true got UNSAT idx=1 trying false got SAT idx=0 trying true got SAT ... run_poor_mans_MaxSMT() begin -> true, val=13
It works slower than if using Open-WBO, but sometimes even faster than Z3!
This is as well: https://github.com/DennisYurichev/random_notes/blob/master/beer_can_optimal_size.md.
And this is close to LEXSAT, see exercise and solution from TAOCP 7.2.2.2:
