Relaxed Survey Propagation for The Weighted Maximum Satisfiability Problem

DOI10.1613/JAIR.2808MaRDI QIDQ3651486zbMATH OpenOpenAlexWikidataFDO

Authors Hai Leong Chieu, Wee Sun Lee

Publication date 10 December 2009

Published in Journal of Artificial Intelligence Research (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1401.3483

zbMATH Keywords

survey propagation algorithm

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Abstract: The survey propagation (SP) algorithm has been shown to work well on large instances of the random 3-SAT problem near its phase transition. It was shown that SP estimates marginals over covers that represent clusters of solutions. The SP-y algorithm generalizes SP to work on the maximum satisfiability (Max-SAT) problem, but the cover interpretation of SP does not generalize to SP-y. In this paper, we formulate the relaxed survey propagation (RSP) algorithm, which extends the SP algorithm to apply to the weighted Max-SAT problem. We show that RSP has an interpretation of estimating marginals over covers violating a set of clauses with minimal weight. This naturally generalizes the cover interpretation of SP. Empirically, we show that RSP outperforms SP-y and other state-of-the-art Max-SAT solvers on random Max-SAT instances. RSP also outperforms state-of-the-art weighted Max-SAT solvers on random weighted Max-SAT instances.

Recommendations

• An efficient solver for weighted Max-SAT
• Principles and Practice of Constraint Programming – CP 2004
• A cooperative search method for the weighted Max-Sat problems
• Survey propagation: An algorithm for satisfiability
• MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability
• Solving the weighted MAX-SAT problem using the dynamic convexized method
• Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems
• Theory and Applications of Satisfiability Testing

Cited in

(3)

• Leveraging cluster backbones for improving MAP inference in statistical relational models
• CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability
• Survey propagation: An algorithm for satisfiability

Describes a project that uses

Uses Software

• UBCSAT
• RSat
• MiniSat

This page was built for publication: Relaxed Survey Propagation for The Weighted Maximum Satisfiability Problem

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3651486)