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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aloul, F.A., Mneimneh, M.N., Sakallah, K.A.: ZBDD-Based Backtrack Search SAT Solver. In: Proceedings of International Workshop on Logic and Synthesis (IWLS), pp. 131–136 (2002)
Biere, A.: Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010. Tech. Rep. 10/1, FMV Reports Series, Institute for Formal Models and Verification, Johannes Kepler University, Altenbergerstr. 69, 4040 Linz, Austria (2010)
Bryant, R.E.: Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers 35(8), 677–691 (1986)
Chatalic, P., Simon, L.: Zres: The old Davis-Putnam procedure meets ZBDDs. In: McAllester, D. (ed.) CADE 2000. LNCS(LNAI), vol. 1831, pp. 449–454. Springer, Heidelberg (2000)
Damiano, R.F., Kukula, J.H.: Checking satisfiability of a conjunction of BDDs. In: 40th Design Automation Conference, DAC 2003, pp. 818–823 (2003)
Dowling, W.F., Gallier, J.H.: Linear-time algorithms for testing the satisfiability of propositional horn formulae. The Journal of Logic Programming 1(3), 267–284 (1984)
Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Ganai, M., Gupta, A.: SAT-Based Scalable Formal Verification Solutions. Series on Integrated Circuits and Systems. Springer-Verlag New York, Inc., Secaucus (2007)
Gopalakrishnan, S., Durairaj, V., Kalla, P.: Integrating CNF and BDD based SAT solvers. In: IEEE International High-Level Design, Validation, and Test Workshop, pp. 51–56 (2003)
Hamadi, Y., Jabbour, S., Sais, L.: ManySAT: a Parallel SAT Solver. Journal on Satisfiability, Boolean Modeling and Computation, Special Issue on Parallel SAT Solving 6, 245–262 (2009)
Huang, J., Darwiche, A.: The Language of Search. Journal of Artificial Intelligence Research 29, 191–219 (2007)
Järvisalo, M., Junttila, T.: Limitations of restricted branching in clause learning. Constraints 14(3), 325–356 (2009)
Kuehlmann, A., Paruthi, V., Krohm, F., Ganai, M.K.: Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification. IEEE Transactions on Computer-Aided Design 21(12), 1377–1394 (2002)
Lee, C.Y.: Representation of Switching Circuits by Binary-Decision Programs. Bell Systems Technical Journal 38, 985–999 (1959)
Lynce, I., Marques-Silva, J.: Efficient data structures for backtrack search SAT solvers. Annals of Mathematics and Artificial Intelligence 43(1), 137–152 (2005)
Marques-Silva, J.P., Sakallah, K.A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers 48(5), 506–521 (1999)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, DAC 2001, pp. 530–535. ACM, New York (2001)
Schubert, T., Lewis, M., Becker, B.: PaMiraXT: Parallel SAT Solving with Threads and Message Passing. Journal on Satisfiability, Boolean Modeling and Computation, Special Issue on Parallel SAT Solving 6, 203–222 (2009)
Semenov, A., Zaikin, O., Bespalov, D., Posypkin, M.: Parallel algorithms for SAT in application to inversion problems of some discrete functions, arXiv:1102.3563v1 [cs.DC]
Soos, M., Nohl, K., Castelluccia, C.: Extending SAT Solvers to Cryptographic Problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244–257. Springer, Heidelberg (2009)
Thakur, R., Rabenseifner, R., Gropp, W.: Optimization of Collective Communication Operations in MPICH. Int’l Journal of High Performance Computing Applications 19(1), 49–66 (2005)
Tseitin, G.: On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic 2, 234–259 (1968)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ignatiev, A., Semenov, A. (2011). DPLL+ROBDD Derivation Applied to Inversion of Some Cryptographic Functions. In: Sakallah, K.A., Simon, L. (eds) Theory and Applications of Satisfiability Testing - SAT 2011. SAT 2011. Lecture Notes in Computer Science, vol 6695. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21581-0_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-21581-0_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21580-3
Online ISBN: 978-3-642-21581-0
eBook Packages: Computer ScienceComputer Science (R0)