diff --git a/src/dimacs/Dagon_dimacs.ml b/src/dimacs/Dagon_dimacs.ml
new file mode 100644
index 00000000..a8adc4f0
--- /dev/null
+++ b/src/dimacs/Dagon_dimacs.ml
@@ -0,0 +1,15 @@
+
+(** {1 Main for dimacs} *)
+
+type 'a or_error = ('a, string) CCResult.t
+
+let parse file : int list list or_error =
+  try
+    CCIO.with_in file
+      (fun ic ->
+         let lexbuf = Lexing.from_channel ic in
+         Parser.file Lexer.token lexbuf)
+    |> CCResult.return
+  with e ->
+    CCResult.of_exn_trace e
+
diff --git a/src/dimacs/Dagon_dimacs.mli b/src/dimacs/Dagon_dimacs.mli
new file mode 100644
index 00000000..e57e16e1
--- /dev/null
+++ b/src/dimacs/Dagon_dimacs.mli
@@ -0,0 +1,13 @@
+
+(** {1 Main for dimacs} *)
+
+(** This library provides a parser for DIMACS files, to represent
+    SAT problems.
+
+    http://www.satcompetition.org/2009/format-benchmarks2009.html
+*)
+
+type 'a or_error = ('a, string) CCResult.t
+
+val parse : string -> int list list or_error
+(** Parse a file into a list of clauses. *)
diff --git a/src/dimacs/Lexer.mll b/src/dimacs/Lexer.mll
new file mode 100644
index 00000000..9a4bb861
--- /dev/null
+++ b/src/dimacs/Lexer.mll
@@ -0,0 +1,22 @@
+(*  Copyright 2005 INRIA  *)
+{
+  open Dagon_util
+  open Parser
+}
+
+let number = ['1' - '9'] ['0' - '9']*
+
+rule token = parse
+  | eof                     { EOF }
+  | "c"                     { comment lexbuf }
+  | [' ' '\t' '\r']         { token lexbuf }
+  | 'p'                     { P }
+  | "cnf"                   { CNF }
+  | '\n'                    { Lexing.new_line lexbuf; token lexbuf }
+  | '0'                     { ZERO }
+  | '-'? number             { LIT (int_of_string (Lexing.lexeme lexbuf)) }
+  | _                       { Util.errorf "dimacs.lexer: unexpected char `%s`" (Lexing.lexeme lexbuf) }
+
+and comment = parse
+  | '\n'                    { Lexing.new_line lexbuf; token lexbuf }
+  | [^'\n']                 { comment lexbuf }
diff --git a/src/dimacs/Parser.mly b/src/dimacs/Parser.mly
new file mode 100644
index 00000000..2386ae2f
--- /dev/null
+++ b/src/dimacs/Parser.mly
@@ -0,0 +1,43 @@
+/*  Copyright 2005 INRIA  */
+
+%{
+  open Dagon_util
+
+  let lnum pos = pos.Lexing.pos_lnum
+  let cnum pos = pos.Lexing.pos_cnum - pos.Lexing.pos_bol
+  let pp_pos out (start,stop) =
+    Format.fprintf out "(at %d:%d - %d:%d)"
+      (lnum start) (cnum start) (lnum stop) (cnum stop)
+%}
+
+%token <int> LIT
+%token ZERO
+%token P CNF EOF
+
+%start file
+%type <int list list> file
+
+%%
+
+/* DIMACS syntax */
+
+prelude:
+  | P CNF LIT LIT { () }
+  | error
+    {
+      Util.errorf "expected prelude %a" pp_pos ($startpos,$endpos)
+    }
+
+clauses:
+  | l=clause* { l }
+  | error
+    {
+      Util.errorf "expected list of clauses %a"
+        pp_pos ($startpos,$endpos)
+    }
+
+file:
+  | prelude l=clauses EOF { l }
+
+clause:
+  | l=LIT+ ZERO { l }
diff --git a/src/dimacs/jbuild b/src/dimacs/jbuild
new file mode 100644
index 00000000..fbc40f44
--- /dev/null
+++ b/src/dimacs/jbuild
@@ -0,0 +1,20 @@
+; vim:ft=lisp:
+
+(jbuild_version 1)
+
+; main binary
+(library
+  ((name dagon_dimacs)
+   (public_name dagon.dimacs)
+   (optional) ; only if deps present
+   (libraries (containers dagon.util))
+   (flags (:standard -w +a-4-42-44-48-50-58-32-60@8))
+   (ocamlopt_flags (:standard -O3 -color always -bin-annot
+                    -unbox-closures -unbox-closures-factor 20))
+  ))
+
+(menhir
+  ((modules (Parser))))
+
+(ocamllex
+  (Lexer))