Equivalence Class Based Parity Reasoning with DPLL(XOR)

Reference:

Tero Laitinen, Tommi Junttila, and Ilkka Niemelä. Equivalence class based parity reasoning with DPLL(XOR). In Taghi M. Khoshgoftaar and Xingquan (Hill) Zhu, editors, ICTAI 2011 - 23rd IEEE International Conference on Tools with Artificial Intelligence, pages 649–658. IEEE Computer Society Press, 2011.

Abstract:

The recently introduced DPLL(XOR) framework for deciding satisfiability of propositional formulas with parity constraints is studied. A new parity reasoning module, based on equivalence class manipulation, is developed and imple- mentation techniques for it described. It is shown that the deduction power of the new module is equivalent to another one proposed earlier. Additional reasoning module independent techniques are presented. Different design choices and module integration strategies are experimentally evaluated on three stream ciphers Trivium, Grain, and Hitag2. The new approach achieves major runtime speedups on the Trivium cipher and significant reduction in the number of decisions on Grain and Hitag2 ciphers.

Suggested BibTeX entry:

@inproceedings{tolaiti2.confictaiLaitinenJN11,
    author = {Tero Laitinen and Tommi Junttila and Ilkka Niemel{\"a}},
    booktitle = {ICTAI 2011 - 23rd IEEE International Conference on Tools with Artificial Intelligence},
    editor = {Taghi M. Khoshgoftaar and Xingquan (Hill) Zhu},
    language = {eng},
    pages = {649-658},
    publisher = {IEEE Computer Society Press},
    title = {Equivalence Class Based Parity Reasoning with {DPLL(XOR)}},
    year = {2011},
}