Core-Guided Binary Search Algorithms for Maximum Satisfiability.
AAAI'11: Proceedings of the Twenty-Fifth AAAI Conference on Artificial Intelligence(2011)
摘要
Several MaxSAT algorithms based on iterative SAT solving have been proposed in recent years. These algorithms are in general the most efficient for real-world applications. Existing data indicates that, among MaxSAT algorithms based on iterative SAT solving, the most efficient ones are core-guided , i.e. algorithms which guide the search by iteratively computing unsatisfiable subformulas (or cores ). For weighted MaxSAT, core-guided algorithms exhibit a number of important drawbacks, including a possibly exponential number of iterations and the use of a large number of auxiliary variables. This paper develops two new algorithms for (weighted) MaxSAT that address these two drawbacks. The first MaxSAT algorithm implements core-guided iterative SAT solving with binary search . The second algorithm extends the first one by exploiting disjoint cores . The empirical evaluation shows that core-guided binary search is competitive with current MaxSAT solvers.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要