Just a few examples. A very pragmatic one: Eclipse includes a SAT solver to manage package dependencies (eg: can package X be installed in version 1.0 and coex

Just a few examples. A very pragmatic one: Eclipse includes a SAT solver to manage package dependencies (eg: can package X be installed in version 1.0 and coexist with package Y with version <= 2.3) SAT is also used for bounded model checking, ie checking whether a given system (hardware or software) is guaranteed to never be in an invalid state. You can have a look at MIT's alloy project (http://alloy.mit.edu/alloy/ http://alloy.mit.edu/alloy/) SAT is sometimes used in cryptography, to try to solve cryptographic problems. SAT solvers are very efficient nowadays, so it often makes sense to translate an NP-complete problem into SAT. This is not always the case, though (some problems would require to generate a huge number of clauses, making the use of a SAT solver impractical).