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 0 or equivalent to WKL 0. 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.