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

2 Citations (Scopus)


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
Number of pages14
ISBN (Print)9783642215803
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


Conference14th International Conference on Theory and Applications of Satisfiability Testing, SAT 2011
Country/TerritoryUnited States of America
CityAnn Arbor

Cite this