Geodesic
Duplicates of conflict clauses in CDCL derivation and their usage to invert some cryptographic functions
Numerical methods and programming, Tome 20 (2019) no. 1, pp. 54-66.

Voir la notice de l'article provenant de la source Math-Net.Ru

A phenomenon of conflict clauses generated repeatedly by SAT solvers is studied. Such clauses may appear during solving hard Boolean satisfiability problems (SAT). This phenomenon is caused by the fact that the modern SAT solvers are based on the CDCL algorithm that generates conflict clauses. A database of such clauses is periodically and partially cleaned. A new approach for practical SAT solving is proposed. According to this approach, the repeatedly generated conflict clauses are tracked, whereas their further generation is prohibited. Based on this approach, a multithreaded SAT solver was developed. This solver was compared with the best multithreaded SAT solvers awarded during the last SAT competitions. According to the experimental results, the developed solver greatly outperforms its competitors on several SAT instances encoding the inversion of some cryptographic hash functions.
Keywords: Boolean satisfiability problem (SAT), CDCL algorithm, conflict clause, cryptographic hash functions. 
@article{VMP_2019_20_1_a5,
     author = {V. S. Kondratiev and A. A. Semenov and O. S. Zaikin},
     title = {Duplicates of conflict clauses in {CDCL} derivation and their usage to invert some cryptographic functions},
     journal = {Numerical methods and programming},
     pages = {54--66},
     publisher = {mathdoc},
     volume = {20},
     number = {1},
     year = {2019},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/VMP_2019_20_1_a5/}
}
TY  - JOUR
AU  - V. S. Kondratiev
AU  - A. A. Semenov
AU  - O. S. Zaikin
TI  - Duplicates of conflict clauses in CDCL derivation and their usage to invert some cryptographic functions
JO  - Numerical methods and programming
PY  - 2019
SP  - 54
EP  - 66
VL  - 20
IS  - 1
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/VMP_2019_20_1_a5/
LA  - ru
ID  - VMP_2019_20_1_a5
ER  - 
%0 Journal Article
%A V. S. Kondratiev
%A A. A. Semenov
%A O. S. Zaikin
%T Duplicates of conflict clauses in CDCL derivation and their usage to invert some cryptographic functions
%J Numerical methods and programming
%D 2019
%P 54-66
%V 20
%N 1
%I mathdoc
%U http://geodesic.mathdoc.fr/item/VMP_2019_20_1_a5/
%G ru
%F VMP_2019_20_1_a5
V. S. Kondratiev; A. A. Semenov; O. S. Zaikin. Duplicates of conflict clauses in CDCL derivation and their usage to invert some cryptographic functions. Numerical methods and programming, Tome 20 (2019) no. 1, pp. 54-66. http://geodesic.mathdoc.fr/item/VMP_2019_20_1_a5/