CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability. Weighted maximum satisfiability and (unweighted) partial maximum satisfiability (PMS) are two significant generalizations of maximum satisfiability (MAX-SAT), and weighted partial maximum satisfiability (WPMS) is the combination of the two, with more important applications in practice. Recently, great breakthroughs have been made on stochastic local search (SLS) for weighted MAX-SAT and PMS, resulting in several state-of-the-art SLS algorithms CCLS, Dist and DistUP. However, compared to the great progress of SLS on weighted MAX-SAT and PMS, the performance of SLS on WPMS lags far behind. In this paper, we present a new SLS algorithm named CCEHC for WPMS. CCEHC employs an extended framework of CCLS with a heuristic emphasizing hard clauses, called EHC. With strong accents on hard clauses, EHC has three components: a variable selection mechanism focusing on configuration checking based only on hard clauses, a weighting scheme for hard clauses, and a biased random walk component. Extensive experiments demonstrate that CCEHC significantly outperforms its state-of-the-art SLS competitors. Further experimental results on comparing CCEHC with a state-of-the-art complete solver show the effectiveness of CCEHC on a number of application WPMS instances, and indicate that CCEHC might be beneficial in practice. Also, empirical analyses confirm the effectiveness of each component underlying the EHC heuristic.
Keywords for this software
References in zbMATH (referenced in 7 articles , 1 standard article )
Showing results 1 to 7 of 7.
- Li, Wenjun; Xu, Chao; Yang, Yongjie; Chen, Jianer; Wang, Jianxin: A refined branching algorithm for the maximum satisfiability problem (2022)
- Xu, Chao; Li, Wenjun; Wang, Jianxin; Yang, Yongjie: An improved algorithm for the ((n, 3))-MaxSAT problem: asking branchings to satisfy the clauses (2021)
- Cai, Shaowei; Lei, Zhendong: Old techniques in new ways: clause weighting, unit propagation and hybridization for maximum satisfiability (2020)
- Chu, Yi; Liu, Boxiao; Cai, Shaowei; Luo, Chuan; You, Haihang: An efficient local search algorithm for solving maximum edge weight clique problem in large graphs (2020)
- Jarvis, Padraigh; Arbelaez, Alejandro: Cooperative parallel SAT local search with path relinking (2020)
- Joshi, Saurabh; Kumar, Prateek; Rao, Sukrut; Martins, Ruben: \textsfOpen-WBO-Inc: approximation strategies for incomplete weighted MaxSAT (2019)
- Luo, Chuan; Cai, Shaowei; Su, Kaile; Huang, Wenxuan: CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability (2017)