@conference{lang1998complexity,
  title={{Complexity results for independence and definability in propositional logic}},
  author={Lang, J. and Marquis, P.},
  booktitle={Pprinciples of Knowlege Representation and Reasoning},
  pages={356--367},
  year={1998},
  organization={Morgan Kaufmann Publishers}
}

@article{thiffault2004solving,
  title={{Solving non-clausal formulas with DPLL search}},
  author={Thiffault, C. and Bacchus, F. and Walsh, T.},
  journal={Principles and Practice of Constraint Programming--CP 2004},
  pages={663--678},
  year={2004},
  publisher={Springer}
}

@techreport{de2007relevancy,
  title={{Relevancy propagation}},
  author={De Moura, L. and Bj{\o}rner, N.},
  number={MSR-TR-2007-140},
  year={2007},
  institution={Microsoft Research}
}

@article{tseitin1968complexity,
  title={{On the complexity of derivation in propositional calculus}},
  author={Tseitin, G.S.},
  journal={Studies in constructive mathematics and mathematical logic},
  volume={2},
  number={115-125},
  pages={10--13},
  year={1968}
}

@conference{cyrluk1997efficient,
  title={{An efficient decision procedure for the theory of fixed-sized bit-vectors}},
  author={Cyrluk, D. and M{\"o}ller, O. and Rue{\ss}, H.},
  booktitle={Computer Aided Verification},
  pages={60--71},
  year={1997},
  organization={Springer}
}

@article{bjorner1998deciding,
  title={{Deciding fixed and non-fixed size bit-vectors}},
  author={Bj{\o}rner, N.S. and Pichora, M.C.},
  journal={Tools and Algorithms for the Construction and Analysis of Systems},
  pages={376},
  year={1998},
  publisher={Springer}
}

@conference{barrett1998decision,
  title={{A decision procedure for bit-vector arithmetic}},
  author={Barrett, C.W. and Dill, D.L. and Levitt, J.R.},
  booktitle={Proceedings of the 35th annual Design Automation Conference},
  pages={522--527},
  isbn={0897919645},
  year={1998},
  organization={ACM}
}

@conference{brinkmann2002rtl,
  title={{RTL-datapath verification using integer linear programming}},
  author={Brinkmann, R. and Drechsler, R.},
  booktitle={Design Automation Conference, 2002. Proceedings of ASP-DAC 2002. 7th Asia and South Pacific and the 15th International Conference on VLSI Design. Proceedings.},
  pages={741--746},
  isbn={0769514413},
  year={2002},
  organization={IEEE}
}

@article{parthasarathy2004efficient,
  title={{An efficient finite-domain constraint solver for circuits}},
  author={Parthasarathy, G. and Iyer, MK and Cheng, K.T. and Wang, L.C.},
  year={2004},
  publisher={ACM}
}

@conference{velev2004efficient,
  title={{Efficient translation of boolean formulas to CNF in formal verification of microprocessors}},
  author={Velev, M.N.},
  booktitle={Proceedings of the 2004 Asia and South Pacific Design Automation Conference},
  pages={310--315},
  isbn={0780381750},
  year={2004},
  organization={IEEE Press}
}

@conference{jackson2005clause,
  title={{Clause form conversions for Boolean circuits}},
  author={Jackson, P. and Sheridan, D.},
  booktitle={Theory and Applications of Satisfiability Testing},
  pages={183--198},
  year={2005},
  organization={Springer}
}

@article{muller2007analysis,
  title={{Analysis of modular arithmetic}},
  author={M{\"u}ller-Olm, M. and Seidl, H.},
  journal={ACM Transactions on Programming Languages and Systems (TOPLAS)},
  volume={29},
  number={5},
  pages={29},
  issn={0164-0925},
  year={2007},
  publisher={ACM}
}

@article{brummayer2006local,
  title={{Local two-level and-inverter graph minimization without blowup}},
  author={Brummayer, R. and Biere, A.},
  journal={Proc. MEMICS},
  volume={6},
  pages={57},
  year={2006},
  publisher={Citeseer}
}

@conference{bruttomesso2007lazy,
  title={{A lazy and layered SMT (BV) solver for hard industrial verification problems}},
  author={Bruttomesso, R. and Cimatti, A. and Franz{\'e}n, A. and Griggio, A. and Hanna, Z. and Nadel, A. and Palti, A. and Sebastiani, R.},
  booktitle={Proceedings of the 19th international conference on Computer aided verification},
  pages={547--560},
  year={2007},
  organization={Springer-Verlag}
}

@article{manolios2007efficient,
  title={{Efficient circuit to CNF conversion}},
  author={Manolios, P. and Vroon, D.},
  journal={Theory and Applications of Satisfiability Testing--SAT 2007},
  pages={4--9},
  year={2007},
  publisher={Springer}
}

@article{bjorner2008modular,
  title={{Modular difference logic is hard}},
  author={Bj{\o}rner, N. and Blass, A. and Gurevich, Y. and Musuvathi, M.},
  journal={Arxiv preprint arXiv:0811.0987},
  year={2008},
  publisher={Citeseer}
}

@article{brummayer2009boolector,
  title={{Boolector: An efficient SMT solver for bit-vectors and arrays}},
  author={Brummayer, R. and Biere, A.},
  journal={Tools and Algorithms for the Construction and Analysis of Systems},
  pages={174--177},
  year={2009},
  publisher={Springer}
}

@conference{bruttomesso2009scalable,
  title={{A scalable decision procedure for fixed-width bit-vectors}},
  author={Bruttomesso, R. and Sharygina, N.},
  booktitle={Proceedings of the 2009 International Conference on Computer-Aided Design},
  pages={13--20},
  year={2009},
  organization={ACM}
}

@conference{jha2009beaver,
  title={{Beaver: Engineering an efficient SMT solver for bit-vector arithmetic}},
  author={Jha, S. and Limaye, R. and Seshia, S.},
  booktitle={Computer Aided Verification},
  pages={668--674},
  year={2009},
  organization={Springer}
}

@article{bardin2010alternative,
  title={{An alternative to SAT-based approaches for bit-vectors}},
  author={Bardin, S. and Herrmann, P. and Perroud, F.},
  journal={Tools and Algorithms for the Construction and Analysis of Systems},
  pages={84--98},
  year={2010},
  publisher={Springer}
}