A Taxonomy of Exact Methods for Partial Max-SAT

被引:4
|
作者
Menai, Mohamed El Bachir [1 ]
Al-Yahya, Tasniem Nasser [1 ]
机构
[1] King Saud Univ, Coll Comp & Informat Sci, Dept Comp Sci, Riyadh 11543, Saudi Arabia
关键词
Partial Max-SAT; Davis-Putnam-Logenmann-Loveland; branch and bound; unsatisfiability; pseudo-Boolean optimization; LOCAL SEARCH; ALGORITHM; SATISFIABILITY;
D O I
10.1007/s11390-013-1325-5
中图分类号
TP3 [计算技术、计算机技术];
学科分类号
0812 ;
摘要
Partial Maximum Boolean Satisfiability (Partial Max-SAT or PMSAT) is an optimization variant of Boolean satisfiability (SAT) problem, in which a variable assignment is required to satisfy all hard clauses and a maximum number of soft clauses in a Boolean formula. PMSAT is considered as an interesting encoding domain to many real-life problems for which a solution is acceptable even if some constraints are violated. Amongst the problems that can be formulated as such are planning and scheduling. New insights into the study of PMSAT problem have been gained since the introduction of the Max-SAT evaluations in 2006. Indeed, several PMSAT exact solvers have been developed based mainly on the Davis-Putnam-Logemann-Loveland (DPLL) procedure and Branch and Bound (B&B) algorithms. In this paper, we investigate and analyze a number of exact methods for PMSAT. We propose a taxonomy of the main exact methods within a general framework that integrates their various techniques into a unified perspective. We show its effectiveness by using it to classify PMSAT exact solvers which participated in the 2007 similar to 2011 Max-SAT evaluations, emphasizing on the most promising research directions.
引用
收藏
页码:232 / 246
页数:15
相关论文
共 50 条
  • [1] A Taxonomy of Exact Methods for Partial Max-SAT
    Mohamed El Bachir Menai
    Tasniem Nasser Al-Yahya
    JournalofComputerScience&Technology, 2013, 28 (02) : 232 - 246
  • [2] A Taxonomy of Exact Methods for Partial Max-SAT
    Mohamed El Bachir Menai
    Tasniem Nasser Al-Yahya
    Journal of Computer Science and Technology, 2013, 28 : 232 - 246
  • [3] Improved exact algorithms for MAX-SAT
    Chen, J
    Kanj, IA
    LATIN 2002: THEORETICAL INFORMATICS, 2002, 2286 : 341 - 355
  • [4] A Two-Phase Exact Algorithm for MAX-SAT and Weighted MAX-SAT Problems
    Borchers B.
    Furman J.
    Journal of Combinatorial Optimization, 1998, 2 (4) : 299 - 306
  • [5] Improved exact algorithms for MAX-SAT
    Chen, JE
    Kanj, IA
    DISCRETE APPLIED MATHEMATICS, 2004, 142 (1-3) : 17 - 27
  • [6] A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems
    Borchers, B
    Furman, J
    JOURNAL OF COMBINATORIAL OPTIMIZATION, 1999, 2 (04) : 299 - 306
  • [7] On solving the Partial MAX-SAT problem
    Fu, Zhaohui
    Malik, Sharad
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2006, PROCEEDINGS, 2006, 4121 : 252 - 265
  • [8] Improved exact solvers for weighted Max-SAT
    Alsinet, T
    Manyà, F
    Planes, J
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING, PROCEEDINGS, 2005, 3569 : 371 - 377
  • [9] Encoding Max-CSP into Partial Max-SAT
    Argelich, Josep
    Cabiscol, Alba
    Lynce, Ines
    Manya, Felip
    38TH INTERNATIONAL SYMPOSIUM ON MULTIPLE-VALUED LOGIC (ISMVL 2008), 2008, : 106 - 111
  • [10] Modelling Max-CSP as partial Max-SAT
    Argelich, Josep
    Cabiscol, Alba
    Lynce, Ines
    Manya, Felip
    THEORY AND APPLICATIONS OF SATISFIABILITY TESTING - SAT 2008, PROCEEDINGS, 2008, 4996 : 1 - +