We use basic combinatorial techniques to count the number of satisfiable boolean formulas given in conjunctive normal form. The intention is to provide information about the relative frequency of boolean functions with respect to statements of a given size. This in turn will provide information about algorithms attempting to decide problems such as satisfiability and validity. The method we use is an explicit counting of those formulas that are satisfiable. We count the number for any boolean function over v variables, k literals per clause and c clauses. First, we describe a correspondence between the syntax of propositions to the semantics of functions using a system of equations. Then we show how to solve such a system.