kcnfs is a dpll based solver. kcnfs integrates a branching variable heuristic devoted essentially to prove the unsatisfiability of random k-sat formulae and which has been inspired by recent statistical physics work. This heuristic waspresented in [DD01] and generalized to solve k-sat formulae with a renormalization strategy in[DD03]. The local techniques called ”picking” first described in [DD01] were implemented in kcnfs.