利用不可满足性求解最大可满足性

是 否 +2 论坛币

k人 参与回答

经管之家送您一份

应届毕业生专属福利!

求职就业群

赵安豆老师微信：zhaoandou666

经管之家联合CDA

送您一个全额奖学金名额~ !

立即领取

感谢您参与论坛问题回答

经管之家送您两个论坛币！

+2 论坛币

摘要翻译：
最大可满足性(MaxSAT)是一种著名的优化方法，有许多实际应用。最广为人知的MAXS AT算法在解决实际应用领域中的困难问题时是无效的。最近的工作提出了利用有效的布尔可满足性(SAT)求解器来解决MaxSAT问题，基于识别和消除不可满足的子公式。然而，这些算法在实践中并不具有可扩展性。分析了现有的基于不可满足子公式辨识的MaxSAT算法。此外，本文还对MaxSAT算法进行了一些关键优化，提出了一种新的替代算法。在实际应用中，所提出的优化和新算法在MaxSAT实例上提供了显着的性能改进。此外，新一代基于不可满足性的MaxSAT求解器的效率有效地反映了现代SAT求解器证明不可满足性和识别不可满足子公式的能力。
---
英文标题：
《On Using Unsatisfiability for Solving Maximum Satisfiability》
---
作者：
Joao Marques-Silva, Jordi Planes
---
最新提交年份：
2007
---
分类信息：

一级分类：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中的材料。
--
一级分类：Computer Science        计算机科学
二级分类：Data Structures and Algorithms        数据结构与算法
分类描述：Covers data structures and analysis of algorithms. Roughly includes material in ACM Subject Classes E.1, E.2, F.2.1, and F.2.2.
涵盖数据结构和算法分析。大致包括ACM学科类E.1、E.2、F.2.1和F.2.2中的材料。
--

---
英文摘要：
  Maximum Satisfiability (MaxSAT) is a well-known optimization pro- blem, with several practical applications. The most widely known MAXS AT algorithms are ineffective at solving hard problems instances from practical application domains. Recent work proposed using efficient Boolean Satisfiability (SAT) solvers for solving the MaxSAT problem, based on identifying and eliminating unsatisfiable subformulas. However, these algorithms do not scale in practice. This paper analyzes existing MaxSAT algorithms based on unsatisfiable subformula identification. Moreover, the paper proposes a number of key optimizations to these MaxSAT algorithms and a new alternative algorithm. The proposed optimizations and the new algorithm provide significant performance improvements on MaxSAT instances from practical applications. Moreover, the efficiency of the new generation of unsatisfiability-based MaxSAT solvers becomes effectively indexed to the ability of modern SAT solvers to proving unsatisfiability and identifying unsatisfiable subformulas.
---
PDF链接：
https://arxiv.org/pdf/0712.1097

扫码加我 拉你入群

请注明：姓名-公司-职位

以便审核进群资格，未注明则拒绝

分享0 收藏0 回帖

关键词：Optimization Applications Presentation Intelligence Improvements proposed based MAXS 提供 识别