On Validating Boolean Optimizers
Antonio Morgado, Joao Marques-Silva

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Testing and Debugging Techniques · Machine Learning and Algorithms
