On Validating Boolean Optimizers
  Boolean optimization finds a wide range of application domains, that
motivated a number of different organizations of Boolean optimizers since the
mid 90s. Some of the most successful approaches are based on iterative calls to
an NP oracle, using either linear search, binary search or the identification
of unsatisfiable sub-formulas. The increasing use of Boolean optimizers in
practical settings raises the question of confidence in computed results. For
example, the issue of confidence is paramount in safety critical settings. One
way of increasing the confidence of the results computed by Boolean optimizers
is to develop techniques for validating the results. Recent work studied the
validation of Boolean optimizers based on branch-and-bound search. This paper
complements existing work, and develops methods for validating Boolean
optimizers that are based on iterative calls to an NP oracle. This entails
implementing solutions for validating both satisfiable and unsatisfiable
answers from the NP oracle. The work described in this paper can be applied to
a wide range of Boolean optimizers, that find application in Pseudo-Boolean
Optimization and in Maximum Satisfiability. Preliminary experimental results
indicate that the impact of the proposed method in overall performance is
negligible.
