On Validating Boolean Optimizers

TL;DR

This paper develops validation techniques for Boolean optimizers based on iterative NP oracle calls, enhancing confidence in their results, especially in safety-critical applications, with minimal impact on performance.

Contribution

It introduces new methods for validating both satisfiable and unsatisfiable results in Boolean optimizers based on iterative NP oracle calls, complementing existing validation approaches.

Findings

Validation methods work for satisfiable and unsatisfiable results.

Impact on overall performance is negligible.

Applicable to Pseudo-Boolean Optimization and MaxSAT.

Abstract

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.