摘要翻译:
布尔优化发现了广泛的应用领域,这促使了自90年代中期以来许多不同的布尔优化器组织。一些最成功的方法是基于对NP oracle的迭代调用,使用线性搜索、二分搜索或识别不可满足的子公式。在实际环境中,布尔优化器的使用越来越多,引起了计算结果可信度的问题。例如,在安全关键环境中,信心问题是最重要的。提高布尔优化器计算结果可信度的一种方法是开发验证结果的技术。最近的工作研究了基于分支定界搜索的布尔优化器的验证。本文补充了现有的工作,并开发了基于对NP Oracle的迭代调用的布尔优化器的验证方法。这需要实现解决方案来验证NP Oracle的可满足和不可满足的答案。本文所述的工作可以应用于广泛的布尔优化器,在伪布尔优化和最大可满足性方面都有应用。初步的实验结果表明,该方法对整体性能的影响可以忽略不计。
---
英文标题:
《On Validating Boolean Optimizers》
---
作者:
Antonio Morgado and Joao Marques-Silva
---
最新提交年份:
2011
---
分类信息:
一级分类:Computer Science 计算机科学
二级分类:Artificial Intelligence
人工智能
分类描述:Covers all areas of AI except Vision, Robotics, Machine Learning, Multiagent Systems, and Computation and Language (Natural Language Processing), which have separate subject areas. In particular, includes Expert Systems, Theorem Proving (although this may overlap with Logic in Computer Science), Knowledge Representation, Planning, and Uncertainty in AI. Roughly includes material in ACM Subject Classes I.2.0, I.2.1, I.2.3, I.2.4, I.2.8, and I.2.11.
涵盖了人工智能的所有领域,除了视觉、机器人、机器学习、多智能体系统以及计算和语言(自然语言处理),这些领域有独立的学科领域。特别地,包括专家系统,定理证明(尽管这可能与计算机科学中的逻辑重叠),知识表示,规划,和人工智能中的不确定性。大致包括ACM学科类I.2.0、I.2.1、I.2.3、I.2.4、I.2.8和I.2.11中的材料。
--
---
英文摘要:
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.
---
PDF链接:
https://arxiv.org/pdf/1109.2752