SAT solving by CSFLOC, the next generation of full-length clause counting algorithms
Gábor Kusper, Csaba Bíró, György Barna Iszály · 2018
In this paper we introduce the CSFLOC algorithm which counts full-length clauses. It is the successor of the Optimized CCC algorithm. By studying Optimized CCC we observed that its full-length clause counter can be increased on its last 1 bit in the best case. As a main contribution we prove that this observation is generally true for Optimized CCC. The new algorithm, CSFLOC, uses this result. It uses also a data structure in which the clauses are ordered by the index of their last literal. These two improvements result in a faster algorithm which can compete with a state-of-the-art SAT solver on problems with lots of clauses, like black-and-white 2-SAT problems and weakly nondecisive SAT problems.