Local Search for Maximum Satisfiability

Maximum Satisfiability (MaxSAT) is the problem of finding an assignment to the variables in a Boolean formula to maximize the number of satisfied clauses.

In weighted MaxSAT, each clause is associated with a positive number as its weight, and the goal is to maximize the total weight of satisfied clauses.

Partial MaxSAT is a significant extension of MaxSAT, in which clauses are divided into hard and soft clauses, and the goal is to satisfy all hard clauses and satisfy the maximum number of soft clauses.

Local search solvers for MaxSAT

Dist is a local search solver for (weighted) Partial MaxSAT. It makes good use of distinction of hard and soft clauses: 1) only weights for hard clauses; 2) separates hard and soft scores.
Dist won four (out of six) partial categories of the incomplete algorithms track of MaxSAT Evaluation 2014, and also won some categories in MaxSAT Evaluation 2015 and 2016.
Please run Dist under Linux 64bit OS.
Reference:
S. Cai, C. Luo, J. Lin, K. Su. New local search methods for partial MaxSAT, Artificial Intelligence 240(2016), 118
CCLS is a local search solver for weighted MaxSAT based on the configuration checking (CC) strategy.
CCLS has won several categories of the incomplete algorithms track of MaxSAT Evaluation 2013, 2014 and 2015.
Running CCLS under Linux 64bit OS: ./CCLS "instance" "seed" "cutoff_time"
Reference:
C. Luo, S. Cai, W. Wu, Z. Jie, K. Su. CCLS: An Efficient Local Search Algorithm for Weighted Maximum Satisfiability, IEEE Transactions on Computers 64(7): 1830-1843 (2015)

Links


Return to homepage.