  Satisfiability problems play a central role in computer science and
engineering as a general framework for studying the complexity of various
problems. Schaefer proved in 1978 that truth satisfaction of propositional
formulas given a language of relations is either NP-complete or tractable. We
classify the corresponding satisfying assignment construction problems in the
framework of reverse mathematics and show that the principles are either
provable over RCA or equivalent to WKL. We formulate also a Ramseyan version of
the problems and state a different dichotomy theorem. However, the different
classes arising from this classification are not known to be distinct.
