| Autor: |
Majalawa, Vie'an Huzair, Utomo, Putranto Hadi, Kusmayadi, Tri Atmojo, Indriati, Diari, Sutrima, Sutrima, Saputro, Dewi Retno Sari |
| Předmět: |
|
| Zdroj: |
AIP Conference Proceedings; 2020, Vol. 2326 Issue 1, p1-7, 7p |
| Abstrakt: |
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. [ABSTRACT FROM AUTHOR] |
| Databáze: |
Complementary Index |
| Externí odkaz: |
|
