Using support vector machine to evaluate usefulness of conflict clauses in CDCL derivation

Abstract

Many state-of-the-art algorithms for solving Boolean satisfiability problem (SAT) are based on the CDCL algorithm. CDCL generates a lot of so-called conflict clauses that correspond to traversed branches of a tree of possible solutions. To maintain high speed of CDCL-based algorithms, it is required to periodically remove some conflict clauses. Therefore, the problem of evaluating conflict clauses usefulness arises. In the present study, a heuristic for solving this problem is proposed that is based on support vector machines. On the first stage, a family of simplified versions of an original SAT instance is constructed, then they are solved via some SAT solver. On the second stage, a support vector machine is trained. During this process, a conflict clause is considered useful if it is not removed at the time of finding a solution of at least one simplified subproblem. On the third stage, an original SAT instance is solved, while the usefulness of some conflict clauses is evaluated by the trained support vector machine. Based on the proposed heuristic, a modified version of a state-of-the-art CDCL solver is implemented. According to the computational experiments, the modified version is more efficient on a few families of hard SAT instances.