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.

@inproceedings{
    conf/ictai/LaitinenJN11_ini,
    editor = "Khoshgoftaar, Taghi M. and Zhu, Xingquan (Hill)",
    author = {Laitinen, Tero and Junttila, Tommi and Niemel{\"a}, Ilkka},
    publisher = "IEEE Computer Society Press",
    language = "eng",
    corerank = "B",
    booktitle = "ICTAI 2011 - 23rd IEEE International Conference on Tools with Artificial Intelligence",
    title = "Equivalence Class Based Parity Reasoning with {DPLL(XOR)}",
    pages = "649-658",
    responsibleauthor = {Laitinen, Tero and Junttila, Tommi and Niemel{\"a}, Ilkka},
    flags = "LOGIC MCM HIIT copy",
    il = "no",
    year = "2011",
    unitcode = "T306=99,T312=1",
    impactfactor = "A4",
    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."
}

AUTHORS:

ABSTRACT: