Knowledge representation is concerned with the design of languages to model broad and diverse problem domains, and with techniques to address general phenomena such as the frame problem, incomplete information and rules with exceptions. The focus of the satisfiability research is on methods to find models of propositional theories. Both areas have made enormous advances: logic programming with the stable-model semantics and ID-logic have matured into expressive and versatile knowledge representation formalisms; clever heuristics, highly specialized data structures and clause learning brought about a new generation of fast satisfiability solvers capable of handling industrial-grade instances. In this talk we explore potential synergies between the two areas. We claim that knowledge representation languages can serve as a programming interface to satisfiability solvers. We argue that the integration of the two areas opens a way to novel and effective declarative programming environments, as evidenced by the emergence of answer-set programming; and gives rise to several promising research directions.