Solution blocking could give exponentially better performance

[msoos]

this part of the code:

    for (i = 1; i <= max_idx; i++)
        mem[i] = (picosat_deref(picosat, i) > 0) ? 1 : -1;

    for (i = 1; i <= max_idx; i++)
        picosat_add(picosat, (mem[i] < 0) ? i : -i);

Doesn't take into account that picosat_deref can return 0. If it returns 0, that variable should not be banned in the clause -- that way, we can ban 2**N solutions in one go (where N is the number of variables that are unset in the solution).

[github-actions]

Hi there, thank you for your contribution!

This issue has been automatically marked as stale because it has not had recent activity. It will be closed automatically if no further activity occurs.

If you would like this issue to remain open please:

1. Verify that you can still reproduce the issue at hand
2. Comment that the issue is still reproducible and include:
   - What OS and version you reproduced the issue on
   - What steps you followed to reproduce the issue

NOTE: If this issue was closed prematurely, please leave a comment.

Thanks!