Conflict driven clause learning approach for satisfiability modulo theory
Vie’an Huzair Majalawa, Putranto Hadi Utomo, Tri Atmojo Kusmayadı, Diari Indriati, Diari Indriati · AIP conference proceedings · 2021
The conflict driven clause learning or CDCL is one of algorithm widely used in a lot of modern SAT solvers. It is because CDCL SAT solvers are so effective in practice, thanks to its non-chronological backjumping and conflict analysis. In this paper, we will discuss about the organization of CDCL solver for SAT solving and how it can be applied for satisfiability modulo theory. We also do experiment on hard-square constraint and found that the computation time using SMT solver follows an exponential function and the precomputation time is not affectedby the increase in the number of blanks.