دانلود رایگان مقاله روش های جستجوی محلی جدید برای MaxSAT جزئی

عنوان فارسی
روش های جستجوی محلی جدید برای MaxSAT جزئی
عنوان انگلیسی
New local search methods for partial MaxSAT
صفحات مقاله فارسی
0
صفحات مقاله انگلیسی
18
سال انتشار
2016
نشریه
الزویر - Elsevier
فرمت مقاله انگلیسی
PDF
کد محصول
E379
رشته های مرتبط با این مقاله
مهندسی کامپیوتر
گرایش های مرتبط با این مقاله
مهندسی نرم افزار و شبکه های کامپیوتری
مجله
هوش مصنوعی - Artificial Intelligence
دانشگاه
دانشکده فنی و مهندسی الکترونیک و علوم کامپیوتر، دانشگاه پکن، چین
کلمات کلیدی
MaxSAT جزئی، جستجوی محلی، امتیاز سخت و نمره، مقداردهی اولیه
۰.۰ (بدون امتیاز)
امتیاز دهید
چکیده

Abstract


Maximum Satisfiability (MaxSAT) is the optimization version of the Satisfiability (SAT) problem. Partial Maximum Satisfiability (PMS) is a generalization of MaxSAT which involves hard and soft clauses and has important real world applications. Local search is a popular approach to solving SAT and MaxSAT and has witnessed great success in these two problems. However, unfortunately, local search algorithms for PMS do not benefit much from local search techniques for SAT and MaxSAT, mainly due to the fact that it contains both hard and soft clauses. This feature makes it more challenging to design efficient local search algorithms for PMS, which is likely the reason of the stagnation of this direction in more than one decade. In this paper, we propose a number of new ideas for local search for PMS, which mainly rely on the distinction between hard and soft clauses. The first three ideas, including weighting for hard clauses, separating hard and soft score, and a variable selection heuristic based on hard and soft score, are used to develop a local search algorithm for PMS called Dist. The fourth idea, which uses unit propagation with priority on hard unit clauses to generate the initial assignment, is used to improve Dist on industrial instances, leading to the DistUP algorithm. The effectiveness of our solvers and ideas is illustrated through experimental evaluations on all PMS benchmarks from the MaxSAT Evaluation 2014. According to our experimental results, Dist shows a significant improvement over previous local search solvers on all benchmarks. We also compare our solvers with state-of-the-art complete PMS solvers and a state-of-the-art portfolio solver, and the results show that our solvers have better performance in random and crafted instances but worse in industrial instances. The good performance of Dist has also been confirmed by the fact that Dist won all random and crafted categories of PMS and Weighted PMS in the incomplete solvers track of the MaxSAT Evaluation 2014.

نتیجه گیری

7. Conclusions and future work


In this work, we proposed a number of novel ideas for local search for Partial MaxSAT, which exploit the distinction between hard and soft clauses. Specifically, we proposed a clause weighting scheme that works only for hard clauses, the idea of separating hard and soft score, and a variable selection heuristic based on hard score and soft score. We then used these ideas to develop a local search algorithm for PMS called Dist. Experimental results show that Dist dramatically outperforms previous local search algorithms. Also, Dist outperforms complete algorithms on random and crafted benchmarks, but is still worse on industrial instances. Further, we proposed an initialization procedure that makes use of unit propagation and puts priority on hard unit clauses, and applied it to improve Dist on industrial instances, resulting in the DistUP solver. Experimental results show that DistUP significantly improves Dist on industrial PMS and WPMS instances, yet it cannot rival state-of-the-art complete solvers. This work made a breakthrough in local search for PMS, which was also confirmed by the excellent performance of Dist in the MaxSAT Evaluation 2014. The strong experimental results suggested that local search based on hard and soft score is a promising direction for solving PMS and deserves further research, and we would like to extend these methods to weighted Partial MaxSAT. Another interesting direction is to study the initialization methods for MaxSAT problems.


بدون دیدگاه