Formal principles, and algorithms for reasoning about knowledge represented in a logical language (e.g., methods used by the state-of-the-art SAT solvers, QBF solvers, and theorem provers, algorithms for knowledge compilation, logical entailment, and model counting), and their applications in computer science (e.g., prediction, diagnosis and testing, planning, model checking, automated theorem proving, constraint satisfaction).