@InProceedings{LaitinenJunttilaNiemela:ICTAI2011,
  author    = {Tero Laitinen and Tommi Junttila and Ilkka Niemel{\"a}},
  title = {Equivalence Class Based Parity Reasoning with {DPLL(XOR)}},
  booktitle = {ICTAI 2011 - 23rd IEEE International Conference on Tools with Artificial Intelligence},
  year = {2011},
  pages = {649--658},
  publisher = {IEEE Computer Society Press},
  editor = {Taghi M. Khoshgoftaar and Xingquan (Hill) Zhu},
  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.
  },
  url = {http://dx.doi.org/10.1109/ICTAI.2011.103}
}

