Author(s)

Huanhuan Peng, Liming Zhang and Ziming Ye

Corresponding Author

Huanhuan Peng

ABSTRACT

The extension rule is a method for solving Boolean Satisfiability (SAT) problems by using maximum terms, but it is not mature enough at present. Many efficient local search algorithms apply true value assignment search solutions. Based on the relationship between extension rules and truth value assignment and some efficient heuristic strategies, this paper mainly does the following three aspects: 1) analyze two different methods of extension rule and truth value assignment and compare them. On this basis, a local search algorithm based on extension rules (LSER) is proposed. 2) Apply configuration checking strategy, propose the greedy search algorithm method (GSER) of extension rules. 3) We also improve the GSER by the subScore strategy and the clause weighting strategy, and design a new strategy called maximum score upper limit strategy. And then a new extension rule method (IGSER) based on greedy local search is proposed. Experiments show that the proposed algorithm outperforms the general extension rule inference method and algorithm GSER on 3-SAT and CBS SAT instances.

KEYWORDS

Boolean Satisfiability (SAT) problem, local search, extension rule, subScore, clause weighting