If you are a newcomer to the SATisfiability problem, you might want to take a look at wikipedia's page on the boolean satisfiability problem first. You might also find those surveys of interest. For a deeper insight of the current interest on SAT solvers for software and hardware verification, Armin Biere's course on formal systems is a good start. Eugene Goldberg has also a nice and somehow non standard way of introducing modern SAT solvers in his three part course on SAT.
Yahoo! has apparently come to the conclusion that since so few uses Boolean anyway, they may as well not support it. That is a mistake. Power-users like librarians, journalists and researchers use them, and they are exactly the kind of people that influences the public opinion in these matters.
R. O'Donnell. (2021)cite arxiv:2105.10386Comment: First edition originally published April 2014, in hardcover book format by Cambridge University Press, and electronically on the author's website. This arXiv version corrects 100+ typos and errors, but is otherwise essentially the same.
R. Wille. Conceptual Structures: Logical, Linguistic, and
Computational Issues, том 1867 из Lecture Notes in Computer Science, Springer, Berlin/Heidelberg, (2000)
A. Waraich. ITiCSE '04: Proceedings of the 9th annual SIGCSE conference on Innovation and technology in computer science education, стр. 97-101. New York, NY, USA, ACM, (2004)