Optimizing with minimum satisfiability
Optimizing with minimum satisfiability
复制标题
DOI：
10.1016/j.artint.2012.05.004
复制
发表时间：
2012-10
期刊：
影响因子：
--
通讯作者：
Chu Min Li;Zhu Zhu-Zhu;F. Manyà;Laurent Simon
中科院分区：
文献类型：
--
作者：
Chu Min Li;Zhu Zhu-Zhu;F. Manyà;Laurent Simon
MinSAT问题是寻找一个真值赋值，使CNF公式中满足条件的子句的数量最小化。当我们区分硬子句和软子句，并且软子句具有相关联的权重时，则称为加权部分MinSAT的问题在于找到满足所有硬子句的真值分配，并且最小化满足的软子句的权重之和。在本文中，我们描述了一个分支定界求解加权部分MinSAT配备了原始的上限，利用集团划分算法和MaxSAT技术。然后，我们报告的实证调查表明，解决组合优化问题，减少他们的MinSAT是一个有竞争力的通用问题解决方法时，解决MaxClique和组合拍卖的情况。最后，我们研究了随机CNF公式的最小满意子句数和最大满意子句数之间的一个有趣的相关性。
MinSAT is the problem of finding a truth assignment that minimizes the number of satisfied clauses in a CNF formula. When we distinguish between hard and soft clauses, and soft clauses have an associated weight, then the problem, called Weighted Partial MinSAT, consists in finding a truth assignment that satisfies all the hard clauses and minimizes the sum of weights of satisfied soft clauses. In this paper we describe a branch-and-bound solver for Weighted Partial MinSAT equipped with original upper bounds that exploit both clique partitioning algorithms and MaxSAT technology. Then, we report on an empirical investigation that shows that solving combinatorial optimization problems by reducing them to MinSAT is a competitive generic problem solving approach when solving MaxClique and combinatorial auction instances. Finally, we investigate an interesting correlation between the minimum number and the maximum number of satisfied clauses on random CNF formulae.