Prover9 SOS Control
Problem: SOS becomes huge, and most of the clauses will never participate in the search
(never be selected as given clauses).
There are two levels of control.
1. Given a limit, say n, on the number of clauses in SOS.
- Cannot simply keep the best n clauses.
- When half full, start being a bit selective.
- When full, be very selective; if kept, discard the worst SOS clause.
2. The SOS limit can be fixed or dynamic. If dynamic,
it is adjusted based on the estimated amount of time left.