Key SAT-related publications

2024

  1. Inverting Cryptographic Hash Functions via Cube-and-Conque. Oleg Zaikin. JAIR [HTML] [PDF]
  2. Inverting step-reduced SHA-1 and MD5 by parameterized SAT solvers. Oleg Zaikin. CP 2024 [HTML] [PDF]

2022

  1. Inverting 43-step MD4 via Cube-and-Conquer. Oleg Zaikin. IJCAI-ECAI 2022 [HTML] [PDF]

2021

  1. Projection heuristics for binary branchings between sum and product. Oliver Kullmann and Oleg Zaikin. SAT 2021 [HTML] [PDF]
  2. Finding effective SAT partitionings via black-box optimization. Alexander Semenov, Oleg Zaikin, and Stepan Kochemazov. Black Box Optimization, Machine Learning, and No-Free Lunch Theorems [HTML] [PDF]

2020

  1. Branch location problems with Maximum Satisfiability. Oleg Zaikin, Alexey Ignatiev, and Joao Marques-Silva ECAI 2020 [HTML] [PDF]
  2. Speeding up CDCL inference with duplicate learnt clauses. Stepan Kochemazov, Oleg Zaikin, Alexander Semenov, and Victor Kondratiev. ECAI 2020 [HTML] [PDF]
  3. Translation of algorithmic descriptions of discrete functions to SAT with applications to cryptanalysis problems. Alexander Semenov, Ilya Otpuschennikov, Irina Gribanova, Oleg Zaikin, and Stepan Kochemazov. Logical methods in computer science [HTML] [PDF]

2019

  1. On black-box optimization in divide-and-conquer SAT solving. Oleg Zaikin and Stepan Kochemazov. Optimization methods and software. [HTML] [PDF]

2018

  1. On cryptographic attacks using backdoors for SAT. Alexander Semenov, Oleg Zaikin, Ilya Otpuschennikov, Stepan Kochemazov. and Alexey Ignatiev AAAI 2018 [HTML] [PDF]
  2. ALIAS: a modular tool for finding backdoors for SAT. Stepan Kochemazov and Oleg Zaikin. SAT 2018 [HTML] [PDF]

2017

  1. An improved SAT-based guess-and-determine attack on the alternating step generator. Oleg Zaikin and Stepan Kochemazov. ISC 2017 [HTML] [PDF]

2016

  1. Algorithm for finding partitionings of hard variants of Boolean satisfiability problem with application to inversion of some cryptographic functions. Alexander Semenov and Oleg Zaikin. SpringerPlus 2016 [HTML] [PDF]
  2. Encoding cryptographic functions to SAT using Transalg system. Ilya Otpuschennikov, Alexander Semenov, Irina Gribanova, Oleg Zaikin, and Stepan Kochemazov. ECAI 2016 [HTML] [PDF]

2015

  1. Using Monte Carlo method for searching partitionings of hard variants of Boolean satisfiability problem. Alexander Semenov and Oleg Zaikin. Parallel Computing Technologies 2015 [HTML] [PDF]

2012

  1. Using BOINC desktop grid to solve large scale SAT problems. Mikhail Posypkin, Alexander Semenov, and Oleg Zaikin. Computer Science [HTML] [PDF]

2011

  1. Parallel logical cryptanalysis of the generator A5/1 in BNB-grid system. Alexander Semenov, Oleg Zaikin, Dmitry Bespalov, and Mikhail Posypkin. Parallel Computing Technologies 2011 [HTML] [PDF]