"Duplicates of conflict clauses in CDCL derivation and their usage to invert some cryptographic functions"
Kondratiev V.S., Semenov A.A., and Zaikin O.S.

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.

  • Kondratiev V.S. – Irkutsk National Research Technical University; ulitsa Lermontova 83, Irkutsk, 664074, Russia; Master’s Student, e-mail: vikseko@gmail.com
  • Semenov A.A. – Matrosov Institute for System Dynamics and Control Theory, Siberian Branch of Russian Academy of Sciences; ulitsa Lermontova 134, Irkutsk, 664033, Russia; Ph.D., Associate Professor, Head of Laboratory, e-mail: biclop.rambler@yandex.ru
  • Zaikin O.S. – Matrosov Institute for System Dynamics and Control Theory, Siberian Branch of Russian Academy of Sciences; ulitsa Lermontova 134, Irkutsk, 664033, Russia; Ph.D., Senior Scientist, e-mail: zaikin.icc@gmail.com