diff --git a/sat/sat.ml b/sat/sat.ml
index 9ef90445..5460fe8d 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -58,6 +58,7 @@ module Fsat = struct
       (if a < 0 then "~" else "")
       (if a mod 2 = 0 then "v" else "f")
       ((abs a) / 2)
+
 end
 
 module Tseitin = Tseitin.Make(Fsat)
@@ -78,4 +79,17 @@ module Make(Dummy : sig end) = struct
     in
     Dot.print out p
 
+  let print_dimacs_clause fmt l =
+    Format.fprintf fmt "%a0" (fun fmt l ->
+        List.iter (fun i -> Format.fprintf fmt "%d " i) l) l
+
+  let print_dimacs fmt l =
+    let l = List.map (fun c ->
+        List.map (fun a -> a.St.lit) @@ Proof.to_list c) l in
+    let n, m = List.fold_left (fun (n, m) c ->
+        let m' = List.fold_left (fun i j -> max i (abs j)) m c in
+        (n + 1, m')) (0, 0) l in
+    Format.fprintf fmt "p cnf %d %d@\n" n m;
+    List.iter (fun c -> Format.fprintf fmt "%a@\n" print_dimacs_clause c) l
+
 end
diff --git a/sat/sat.mli b/sat/sat.mli
index d830b3cd..bcc87f68 100644
--- a/sat/sat.mli
+++ b/sat/sat.mli
@@ -55,5 +55,8 @@ module Make(Dummy : sig end) : sig
   val print_proof : Format.formatter -> Proof.proof -> unit
   (** Print the given proof in dot format. *)
 
+  val print_dimacs : Format.formatter -> St.clause list -> unit
+  (** Prints a cnf in dimacs format on the given formatter *)
+
 end