Optimizing with minimum satisfiability

被引：46

作者：

Li, Chu Min ^{[1
,2
]}

Zhu, Zhu ^{[1
]}

Manya, Felip ^{[3
]}

Simon, Laurent ^{[4
]}

机构：

[1] Univ Picardie Jules Verne, MIS, F-80000 Amiens, France

[2] Huazhong Univ Sci & Technol, Wuhan 430074, Peoples R China

[3] CSIC, Spanish Sci Res Council, Artificial Intelligence Res Inst IIIA, Bellaterra 08193, Spain

[4] Parc Club Univ, LRI, INRIA Futurs, F-91893 Orsay, France

来源：

ARTIFICIAL INTELLIGENCE | 2012年 / 190卷

基金：

中国国家自然科学基金;

关键词：

Satisfiability; MinSAT; MaxSAT; Combinatorial optimization; Branch-and-bound; BOUND ALGORITHM;

D O I：

10.1016/j.artint.2012.05.004

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

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. (c) 2012 Elsevier B.V. All rights reserved.

引用

页码：32 / 44

页数：13

共 22 条

[1] [Anonymous], 2008, J. Satisf. Boolean Model. Comput
[2] Approximating MIN 2-SAT and MIN 3-SAT
Avidor, A
Zwick, U
[J]. THEORY OF COMPUTING SYSTEMS, 2005, 38 (03) : 329 - 345
[3] Combining Graph Structure Exploitation and Propositional Reasoning for the Maximum Clique Problem
Li, Chu-Min
Quan, Zhe
[J]. 22ND INTERNATIONAL CONFERENCE ON TOOLS WITH ARTIFICIAL INTELLIGENCE (ICTAI 2010), PROCEEDINGS, VOL 1, 2010,
[4] Fujishima Y, 1999, IJCAI-99: PROCEEDINGS OF THE SIXTEENTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE, VOLS 1 & 2, P548
[5] Heras F., 2008, Journal on Satisfiability, Boolean Modeling and Computation, V4, P239, DOI 10.3233/sat190046
[6] THE MINIMUM SATISFIABILITY PROBLEM
KOHLI, R
KRISHNAMURTI, R
MIRCHANDANI, P
[J]. SIAM JOURNAL ON DISCRETE MATHEMATICS, 1994, 7 (02) : 275 - 283
[7] Konc J, 2007, MATCH-COMMUN MATH CO, V58, P569
[8] Kugel A., 2012, P LEARN INT OPT C LI
[9] Kugel A., 2010, P WORKSH PRAGM SAT
[10] Leyton-Brown K., 2000, EC'00. Proceedings of the 2nd ACM Conference on Electronic Commerce, P66, DOI 10.1145/352871.352879

← 1 2 3 →