Analyzing Multiple Conflicts in SAT: An Experimental Evaluation.

Unit propagation and conflict analysis are two essential ingredients of CDCL SAT Solving. The order in which unit propagation is computed does not matter when no conflict is found, because it is well known that there exists a unique unit-propagation fixpoint. However, when a conflict is found, current CDCL implementations stop and analyze that concrete conflict, even though other conflicts may exist in the unit-propagation closure. In this experimental evaluation, we report on our experience in modifying this concrete aspect in the CaDiCaL SAT Solver and try to answer the question of whether we can improve the performance of SAT Solvers by the analysis of multiple conflicts.