Equivalence Class Based Parity Reasoning with DPLL(XOR) (2011)
AUTHORS:
Laitinen Tero
,
Junttila Tommi
,
Niemelä Ilkka
BOOKTITLE:
ICTAI 2011 - 23rd IEEE International Conference on Tools with Artificial Intelligence
PAGES:
649-658
@inproceedings{ conf/ictai/LaitinenJN11, 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", title = "Equivalence Class Based Parity Reasoning with {DPLL(XOR)}", booktitle = "ICTAI 2011 - 23rd IEEE International Conference on Tools with Artificial Intelligence", corerank = "B", 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.", 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", pages = "649-658" }