DPLL+ROBDD derivation applied to inversion of some cryptographic functions

Alexey Ignatiev, Alexander A. Semenov

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

1 Citation (Scopus)

Abstract

The paper presents logical derivation algorithms that can be applied to inversion of polynomially computable discrete functions. The proposed approach is based on the fact that it is possible to organize DPLL derivation on a small subset of variables appeared in a CNF which encodes the algorithm computing the function. The experimental results showed that arrays of conflict clauses generated by this mode of derivation, as a rule, have efficient ROBDD representations. This fact is the departing point of development of a hybrid DPLL+ROBDD derivation strategy: derivation techniques for ROBDD representations of conflict databases are the same as those ones in common DPLL (variable assignments and unit propagation). In addition, compact ROBDD representations of the conflict databases can be shared effectively in a distributed computing environment.

Original languageEnglish
Title of host publicationTheory and Application of Satisfiability Testing - 14th International Conference, SAT 2011, Proceedings
PublisherSpringer
Pages76-89
Number of pages14
Volume6695
ISBN (Print)9783642215803
DOIs
Publication statusPublished - 2011
Externally publishedYes
Event14th International Conference on Theory and Applications of Satisfiability Testing, SAT 2011 - Ann Arbor, United States of America
Duration: 19 Jun 201122 Jun 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6695 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference14th International Conference on Theory and Applications of Satisfiability Testing, SAT 2011
CountryUnited States of America
CityAnn Arbor
Period19/06/1122/06/11

Cite this

Ignatiev, A., & Semenov, A. A. (2011). DPLL+ROBDD derivation applied to inversion of some cryptographic functions. In Theory and Application of Satisfiability Testing - 14th International Conference, SAT 2011, Proceedings (Vol. 6695, pp. 76-89). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 6695 LNCS). Springer. https://doi.org/10.1007/978-3-642-21581-0_8