SAT has played a key role in diverse areas spanning testing, formal verification, planning, inferencing and the like. Apart from the classical problem of checking boolean, the problems of generating satisfying uniformly at random, of counting the total number of satisfying assignments have also attracted significant theoretical and practical interest over the years. Prior work offered heuristic approaches with no guarantee of performance, and theoretical approaches with proven guarantees, but poor performance in practice. In this talk, I will describe a novel approach based on limited independent hashing and present two practical algorithms, UniformWitness and approxMC, for solving these two fundamental problems. Our algorithms work by issuing polynomial calls to SAT solver. Unlike prior work, our algorithms provide strong theoretical guarantees and also scale to practical problem sizes.