国家自然科学基金项目(61872159,61672261,61502199)
[1] Li C M, Manya F, Planes J. New Inference Rules for Max-SAT. jair, 2007, 30: 321-359 CrossRef Google Scholar
[2] Lin H, Su K, Li C M. Within-problem learning for efficient lower bound computation in Max-SAT solving. In: Proceedings of the 23rd AAAI Conference of Artificial Intelligence, Chicago, 2008. 351--356. Google Scholar
[3] Heras F, Larrosa J, Oliveras A. MiniMaxSAT: An Efficient Weighted Max-SAT solver. jair, 2008, 31: 1-32 CrossRef Google Scholar
[4] Davies J, Cho J, Bacchus F. Using learnt clauses in MAXSAT. In: Proceedings of the 16th International Conference of Principles and Practice of Constraint Programming - CP 2010, St. Andrews, 2010. 176--190. Google Scholar
[5] Li C M, Manyà F, Mohamedou N, et al. Exploiting cycle structures in Max-SAT. In: Proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing, Swansea, 2009. 467--480. Google Scholar
[6] Ansótegui C, Bonet M L, Levy J. SAT-based MaxSAT algorithms. Artificial Intelligence, 2013, 196: 77-105 CrossRef Google Scholar
[7] Martins R, Manquinho V, Lynce I. Community-based partitioning for MaxSAT solving. In: Proceeding of the 16th International Conference of Theory and Applications of Satisfiability Testing (SAT 2013), Helsinki, 2013. 182--191. Google Scholar
[8] Narodytska N, Bacchus F. Maximum satisfiability using core-guided MAXSAT resolution. In: Proceeding of the 28th AAAI Conference on Artificial Intelligence, Québec City, 2014. 2717--2723. Google Scholar
[9] Fu Z, Malik S. On solving the partial MAX-SAT problem. In: Proceeding of the 9th International Conference of Theory and Applications of Satisfiability Testing, Seattle, 2006. 252--265. Google Scholar
[10] Davies J, Bacchus F. Solving MAXSAT by solving a sequence of simpler SAT instances. In: Proceeding of the 17th International Conference of Principles and Practice of Constraint Programming (CP 2011), Perugia, 2011. 225--239. Google Scholar
[11] Koshimura M, Zhang T, Fujita H, et al. QMaxSAT: A partial Max-SAT solver. J Satisf Boolean Model, 2012, 8: 95--100. Google Scholar
[12] Cai S W, Luo C, Zhang H. From decimation to local search and back: A new approach to MaxSAT. In: Proceeding of the 26th International Joint Conference on Atificial Intelligence, Melbourne, 2017. 571--577. Google Scholar
[13] Morgado A, Heras F, Liffiton M. Iterative and core-guided MaxSAT solving: A survey and assessment. Constraints, 2013, 18: 478-534 CrossRef Google Scholar
[14] Luo C, Cai S W, Wu W. CCLS: An Efficient Local Search Algorithm for Weighted Maximum Satisfiability. IEEE Trans Comput, 2015, 64: 1830-1843 CrossRef Google Scholar
[15] Cai S W, Luo C, Lin J K. New local search methods for partial MaxSAT. Artificial Intelligence, 2016, 240: 1-18 CrossRef Google Scholar
[16] Robinson J A, Davis M, Logemann G, et al. A machine program for theorem-proving. J Symb Log, 1967, 32: 118. Google Scholar
[17] Biere A, Heule M, Maaren H V, et al. Handbook of Satisfiability. Netherlands: IOS Press, 2009. 99--130. Google Scholar
[18] Reiter R. A theory of diagnosis from first principles. Artificial Intelligence, 1987, 32: 57-95 CrossRef Google Scholar
[19] Chieu H L, Lee W S. Relaxed Survey Propagation for The Weighted Maximum Satisfiability Problem. jair, 2009, 36: 229-266 CrossRef Google Scholar
[20] Wang Y, Cai S, Yin M. Two efficient local search algorithms for maximum weight clique problem. In: Proceeding of Proceedings of the 30th AAAI Conference on Atificial Intelligence, Phoenix, 2016. 805--811. Google Scholar
Figure 1
Boolean circuit
Figure 2
(Color online) Number of soft blocking variables for 258 test instances
Figure 3
(Color online) Comparison of SCPMS algorithms with different stop mechanisms and different flip variables and solutions of soft blocking vars
Figure 4
(Color online) Comparison of DeciDist and SCPMS algorithms with different stop mechanisms and different flip times
Benchmark | $\#$ Inst | DistUP #Win. | DeciDist #Win. | SCPMS #Win. | WPM3 #Win. |
b14 | 26 | 0 | 0 | 18 | 12 |
b15 | 6 | 0 | 0 | 1 | 6 |
b17 | 26 | 0 | 0 | 8 | 26 |
b20 | 64 | 0 | 0 | 18 | 58 |
b21 | 120 | 0 | 0 | 21 | 115 |
b22 | 55 | 0 | 0 | 8 | 55 |
Hard_unit_clause_Propagation(); |
Soft_unit_clause_Propagation(); |
($\nexists$ unit clause) $v$ $\leftarrow$ a randomly unassigned vars; |
Assign($v$); |
Benchmark | $\#$ Inst. | Maximum | Minimum | Mean |
b14 | 26 | 33 | 20 | 25 |
b15 | 6 | 37 | 28 | 30 |
b17 | 26 | 40 | 21 | 38 |
b20 | 64 | 39 | 22 | 32 |
b21 | 120 | 39 | 21 | 27 |
b22 | 55 | 40 | 22 | 33 |
$\alpha\ast$ $\leftarrow~$ Decimation($F$); |
cost$\ast$ $\leftarrow~$ $+\propto$; |
|
$\alpha~\ast~\leftarrow~\alpha$; |
cost$\ast$ $\leftarrow~$ cost($\alpha$); |
|
|
$\alpha\ast$ $\leftarrow~$ $\alpha$; |
cost$\ast$ $\leftarrow~$ cost($\alpha$); |
|
|
$V$ $\leftarrow~$ a variable in $S$ with the greatest sscore, breaking ties randomly; |
|
|
Update weights of hard clauses according to HPAWS; |
|
|
$c$ $\leftarrow$ a random falsified hard clause; |
|
$c$ $\leftarrow~$ a random falsified soft clause; |
|
|
$v$ $\leftarrow~$ a random variable in $c$; |
|
$v$ $\leftarrow~$ a variable in c with the greatest sscore; |
$\alpha$ $\leftarrow~$ $\alpha$ with $v$ flipped; |
|
|
return (cost$\ast$, $\alpha\ast$); |
|
return “no feasible assignment found"; |
|
New CNF formula $F$ $\leftarrow~$ chooseHClausedel(CNF, DelHClause); |
Vars $\leftarrow~$ DPLL($F$); |
choosedHVQueue $\leftarrow~$ Compare(DelHClause, Vars); |
$V$ $\leftarrow~$ choosedHVQueue.pop(); |
sv $\leftarrow~$ ChooseSClauseVar($v$); |
choosedSVQueue(sv); |
Return a choosedSVQueue; |
$Q$ $\leftarrow~$ CSV($F$); |
var $\leftarrow~$ $Q$.pop(); |
Filp(var); |
UnitPropagate(Hvar); |
UnitPropagate(Svar); |
Assign var with a random number from 0,1; |
LocalSearch(); |