make SAT.PBO.* more uniform
implement core-guided binary search algorithm with disjoint cores (BCD algorithm)
retain learnt constraints in binary and adaptive searches, while removing old upper bound constraints