SCIENCE CHINA Information Sciences, Volume 60, Issue 9: 092109(2017) https://doi.org/10.1007/s11432-016-0258-4

A randomized diversification strategy for solving satisfiability problem with long clauses

More info
  • ReceivedAug 4, 2016
  • AcceptedSep 12, 2016
  • PublishedMay 11, 2017


Satisfiability problem (SAT) is a central problem in artificial intelligence due to its computational complexity and usefulness in industrial applications. Stochastic local search (SLS) algorithms are powerful to solve hard instances of satisfiability problems, among which CScoreSAT is proposed for solving SAT instances with long clauses by using greedy mode and diversification mode. In this paper, we present a randomized variable selection strategy to improve efficiency of the diversification mode, and thus propose a new SLS algorithm. We perform a number of experiments to evaluate the new algorithm comparing with the recently proposed algorithms, and show that our algorithm is comparative with others for solving random instances near the phase transition threshold.


    Algorithm 1 CScoreSAT

    Input CNF-formula F, maxSteps;

    output a solution or “unknown”;

    $\alpha \gets$ randomly generated truth assignment;

    for step $\gets $ 1 to maxSteps

    if $\alpha$ satisfies $F$ then

    return $\alpha$;

    end if

    if $S=\{x|x$ is comprehensively decreasing and configuration changed$\}$ is not empty then

    $v \gets $ a variable in $S$ with the greatest cscore, breaking ties in favor of the one with largest age;


    update clause weights according to PAWS;

    pick a random falsified clause $C$;

    $v\gets$ the variable in $C$ with the greatest hscore;

    end if

    $\alpha \gets \alpha$

    with $v$ flipped;

Copyright 2019 Science China Press Co., Ltd. 《中国科学》杂志社有限责任公司 版权所有