@Misc{gensat,
	title = {SAT Instance Generation Page},
	note = {\\\verb+http://www.is.titech.ac.jp/~watanabe/gensat/+}	
}
@Misc{rsat,
	title = {RSAT Homepage},
	note = {\verb+http://reasoning.cs.ucla.edu/rsat/index.html+}	
}
@misc{balcarek,
	author = {Jiří Balcárek},
	title = {Řešení problému splnitelnosti booleovské formule (SAT) pomocí binárních rozhodovacích diagramů (BDD)},
	note = {Bakalářská práce, FEL ČVUT v Praze},
	year = {2007}
}
@misc{toman,
	author = {David Toman},
	title = {Nástroj pro manipulaci s logickými funkcemi popsanými algebraickým výrazem},
	note = {Bakalářská práce, FEL ČVUT v Praze},
	year = {2007}
}
@Misc{satcomp,
    author = {},
    title = {The international SAT Competitions},
    note = {\verb+http://www.satcompetition.org/+}
}
@Misc{satlive,
    author = {},
    title = {Links for the SATisfiability Problem},
    note = {\verb+http://www.satlive.org/+}
}
@Misc{dimacs,
	title = {DIMACS CNF formát},
	note = {\\\verb+ftp://dimacs.rutgers.edu/pub/challenge/sat/doc+}
}
@Misc{bench,
	title = {DIMACS benchmarks},
	note = {\\\verb+ftp://dimacs.rutgers.edu/pub/challenge/sat/benchmarks/cnf+}
}
@Misc{dpalg,
    title = {DP algorithm pseudocode},
    note = {\footnotesize\\\verb+ira.informatik.uni-freiburg.de/+
			\verb+~herbstri/publications/HB_2003/img5.html+\normalsize}
}
@article{bdd,
    author = {Randal E. Bryant},
    title = {Graph-Based Algorithms for Boolean Function Manipulation},
    journal = {{IEEE} Transactions on Computers},
    volume = {35},
    number = {8},
    pages = {677--691},
    year = {1986}
}
@inproceedings{cook,
    author = {Stephen A. Cook},
    title = {The complexity of theorem-proving procedures},
    booktitle = {Proceedings of the third annual ACM symposium on Theory of computing},
    year = {1971},
    pages = {151--158},
    location = {Shaker Heights, Ohio, United States},
    doi = {http://doi.acm.org/10.1145/800157.805047},
    publisher = {ACM Press},
    address = {New York, NY, USA},
}
@article{dll,
    author = {Martin Davis and George Logemann and Donald Loveland},
    title = {A machine program for theorem-proving},
    journal = {Commun. ACM},
    volume = {5},
    number = {7},
    year = {1962},
    issn = {0001-0782},
    pages = {394--397},
    doi = {http://doi.acm.org/10.1145/368273.368557},
    publisher = {ACM Press},
    address = {New York, NY, USA},
}
@article{dp,
    author = {Martin Davis and Hilary Putnam},
    title = {A Computing Procedure for Quantification Theory},
    journal = {J. ACM},
    volume = {7},
    number = {3},
    year = {1960},
    issn = {0004-5411},
    pages = {201--215},
    doi = {http://doi.acm.org/10.1145/321033.321034},
    publisher = {ACM Press},
    address = {New York, NY, USA},
}
@inproceedings{hoos,
    author = {Holger H. Hoos},
    title = {On the Run-Time Behaviour of Stochastic Local Search Algorithms for {SAT}},
    booktitle = {Proceedings of the Sixteenth National Conference on Artificial Intelligence ({AAAI}'99)},
    address = {Orlando, Florida},
    pages = {661--666},
    year = {1999}
}
@inproceedings{grasp,
    author = {Jo{\~a}o P. Marques-Silva and Karem A. Sakallah},
    title = {{GRASP - A New Search Algorithm for Satisfiability}},
    booktitle = {Proceedings of {IEEE}/{ACM} International Conference on Computer-Aided Design},
    pages = {220--227},
    year = {1996}
}
@inproceedings{localsearch,
    author = {Bart Selman and Henry A. Kautz and Bram Cohen},
    title = {Local Search Strategies for Satisfiability Testing},
    booktitle = {DIMACS Series in Discrete Mathematics and Theoretical Computer Science},
    volume = {26},
    pages = {521--532},
    year = {1996}
}
@inproceedings{walksat,
    author = {David McAllester and Bart Selman and Henry Kautz},
    title = {Evidence for Invariants in Local Search},
    booktitle = {Proceedings of the Fourteenth National Conference on Artificial Intelligence ({AAAI}'97)},
    address = {Providence, Rhode Island},
    pages = {321--326},
    year = {1997}
}
@inproceedings{chaff,
    author = {Matthew W. Moskewicz and Conor F. Madigan and Ying Zhao and Lintao Zhang and Sharad Malik},
    title = {{Chaff: Engineering an Efficient {SAT} Solver}},
    booktitle = {Proceedings of the 38th Design Automation Conference ({DAC}'01)},
    year = {2001}
}
@article{stalmarck,
    author = {Mary Sheeran and Gunnar St{\aa}lmark},
    title = {A tutorial on St{\aa}lmark's proof procedure for propositional logic},
    journal = {Formal Methods in System Design},
    volume = {16},
    pages = {23--58},
    year = {2000}
}
@inproceedings{force,
    author = {F. Aloul and I. Markov and K. Sakallah},
    title = {FORCE: A Fast and Easy-To-Implement Variable-Ordering Heuristic},
    booktitle = {Proceedings of the 13th ACM Great Lakes Symposium on VLSI 2003},
    pages = {116--119},
    year = {2003}
}
@misc{nanosat,
	author = {Armin Biere},
	title = {The Evolution from LIMMAT to NANOSAT},
	note = {Technical Report No. 444, Dept. Computer Science, ETH Zurich, CH-8092 Zurich, Switzerland},
	year = {2004}
}
@misc{minisat,
	author = {Niklas Eén and Niklas Sörensson},
	title = {An Extensible SAT-solver},
	year = {2003}
}
@misc{jerusat,
	author = {Alexander Nadel},
	title = {Backtrack Search Algorithms for Propositional Logic Satisfiability : Review and Innovations},
	note = {Master Thesis, The Hebrew University},
	year = {2002}
}
@inproceedings{ve,
 	author = {Jinbo Huang and Adnan Darwiche},
 	title = {Toward Good Elimination Orders for Symbolic SAT Solving},
 	booktitle = {ICTAI '04: Proceedings of the 16th IEEE International Conference on Tools with Artificial Intelligence (ICTAI'04)},
	 year = {2004},
 	pages = {566--573},
 	publisher = {IEEE Computer Society},
 	address = {Washington, DC, USA}
 }