\begin{thebibliography}{10}

\bibitem{bench}
Dimacs benchmarks.
\newblock \\\verb+ftp://dimacs.rutgers.edu/pub/challenge/sat/benchmarks/cnf+.

\bibitem{dimacs}
Dimacs cnf formát.
\newblock \\\verb+ftp://dimacs.rutgers.edu/pub/challenge/sat/doc+.

\bibitem{dpalg}
Dp algorithm pseudocode.
\newblock \footnotesize\\\verb+ira.informatik.uni-freiburg.de/+
  \verb+~herbstri/publications/HB_2003/img5.html+\normalsize.

\bibitem{satcomp}
The international sat competitions.
\newblock \verb+http://www.satcompetition.org/+.

\bibitem{satlive}
Links for the satisfiability problem.
\newblock \verb+http://www.satlive.org/+.

\bibitem{rsat}
Rsat homepage.
\newblock \verb+http://reasoning.cs.ucla.edu/rsat/index.html+.

\bibitem{gensat}
Sat instance generation page.
\newblock \\\verb+http://www.is.titech.ac.jp/~watanabe/gensat/+.

\bibitem{force}
F.~Aloul, I.~Markov, and K.~Sakallah.
\newblock Force: A fast and easy-to-implement variable-ordering heuristic.
\newblock In {\em Proceedings of the 13th ACM Great Lakes Symposium on VLSI
  2003}, pages 116--119, 2003.

\bibitem{balcarek}
Jiří Balcárek.
\newblock Řešení problému splnitelnosti booleovské formule (sat) pomocí
  binárních rozhodovacích diagramů (bdd), 2007.
\newblock Bakalářská práce, FEL ČVUT v Praze.

\bibitem{nanosat}
Armin Biere.
\newblock The evolution from limmat to nanosat, 2004.
\newblock Technical Report No. 444, Dept. Computer Science, ETH Zurich, CH-8092
  Zurich, Switzerland.

\bibitem{bdd}
Randal~E. Bryant.
\newblock Graph-based algorithms for boolean function manipulation.
\newblock {\em {IEEE} Transactions on Computers}, 35(8):677--691, 1986.

\bibitem{cook}
Stephen~A. Cook.
\newblock The complexity of theorem-proving procedures.
\newblock In {\em Proceedings of the third annual ACM symposium on Theory of
  computing}, pages 151--158, New York, NY, USA, 1971. ACM Press.

\bibitem{dll}
Martin Davis, George Logemann, and Donald Loveland.
\newblock A machine program for theorem-proving.
\newblock {\em Commun. ACM}, 5(7):394--397, 1962.

\bibitem{dp}
Martin Davis and Hilary Putnam.
\newblock A computing procedure for quantification theory.
\newblock {\em J. ACM}, 7(3):201--215, 1960.

\bibitem{minisat}
Niklas Eén and Niklas Sörensson.
\newblock An extensible sat-solver, 2003.

\bibitem{hoos}
Holger~H. Hoos.
\newblock On the run-time behaviour of stochastic local search algorithms for
  {SAT}.
\newblock In {\em Proceedings of the Sixteenth National Conference on
  Artificial Intelligence ({AAAI}'99)}, pages 661--666, Orlando, Florida, 1999.

\bibitem{ve}
Jinbo Huang and Adnan Darwiche.
\newblock Toward good elimination orders for symbolic sat solving.
\newblock In {\em ICTAI '04: Proceedings of the 16th IEEE International
  Conference on Tools with Artificial Intelligence (ICTAI'04)}, pages 566--573,
  Washington, DC, USA, 2004. IEEE Computer Society.

\bibitem{grasp}
Jo{\~a}o~P. Marques-Silva and Karem~A. Sakallah.
\newblock {GRASP - A New Search Algorithm for Satisfiability}.
\newblock In {\em Proceedings of {IEEE}/{ACM} International Conference on
  Computer-Aided Design}, pages 220--227, 1996.

\bibitem{walksat}
David McAllester, Bart Selman, and Henry Kautz.
\newblock Evidence for invariants in local search.
\newblock In {\em Proceedings of the Fourteenth National Conference on
  Artificial Intelligence ({AAAI}'97)}, pages 321--326, Providence, Rhode
  Island, 1997.

\bibitem{chaff}
Matthew~W. Moskewicz, Conor~F. Madigan, Ying Zhao, Lintao Zhang, and Sharad
  Malik.
\newblock {Chaff: Engineering an Efficient {SAT} Solver}.
\newblock In {\em Proceedings of the 38th Design Automation Conference
  ({DAC}'01)}, 2001.

\bibitem{jerusat}
Alexander Nadel.
\newblock Backtrack search algorithms for propositional logic satisfiability :
  Review and innovations, 2002.
\newblock Master Thesis, The Hebrew University.

\bibitem{localsearch}
Bart Selman, Henry~A. Kautz, and Bram Cohen.
\newblock Local search strategies for satisfiability testing.
\newblock In {\em DIMACS Series in Discrete Mathematics and Theoretical
  Computer Science}, volume~26, pages 521--532, 1996.

\bibitem{stalmarck}
Mary Sheeran and Gunnar St{\aa}lmark.
\newblock A tutorial on st{\aa}lmark's proof procedure for propositional logic.
\newblock {\em Formal Methods in System Design}, 16:23--58, 2000.

\bibitem{toman}
David Toman.
\newblock Nástroj pro manipulaci s logickými funkcemi popsanými algebraickým
  výrazem, 2007.
\newblock Bakalářská práce, FEL ČVUT v Praze.

\end{thebibliography}
