diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000..dbbc8f1
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for sift
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.
diff --git a/examples/coloring-petersen3.cnf b/examples/coloring-petersen3.cnf
new file mode 100644
index 0000000..af9060f
--- /dev/null
+++ b/examples/coloring-petersen3.cnf
@@ -0,0 +1,87 @@
+c Petersen graph 3-coloring, SAT
+p cnf 30 85
+1 2 3 0
+-1 -2 0
+-1 -3 0
+-2 -3 0
+4 5 6 0
+-4 -5 0
+-4 -6 0
+-5 -6 0
+7 8 9 0
+-7 -8 0
+-7 -9 0
+-8 -9 0
+10 11 12 0
+-10 -11 0
+-10 -12 0
+-11 -12 0
+13 14 15 0
+-13 -14 0
+-13 -15 0
+-14 -15 0
+16 17 18 0
+-16 -17 0
+-16 -18 0
+-17 -18 0
+19 20 21 0
+-19 -20 0
+-19 -21 0
+-20 -21 0
+22 23 24 0
+-22 -23 0
+-22 -24 0
+-23 -24 0
+25 26 27 0
+-25 -26 0
+-25 -27 0
+-26 -27 0
+28 29 30 0
+-28 -29 0
+-28 -30 0
+-29 -30 0
+-1 -4 0
+-2 -5 0
+-3 -6 0
+-4 -7 0
+-5 -8 0
+-6 -9 0
+-7 -10 0
+-8 -11 0
+-9 -12 0
+-10 -13 0
+-11 -14 0
+-12 -15 0
+-13 -1 0
+-14 -2 0
+-15 -3 0
+-16 -22 0
+-17 -23 0
+-18 -24 0
+-22 -28 0
+-23 -29 0
+-24 -30 0
+-28 -19 0
+-29 -20 0
+-30 -21 0
+-19 -25 0
+-20 -26 0
+-21 -27 0
+-25 -16 0
+-26 -17 0
+-27 -18 0
+-1 -16 0
+-2 -17 0
+-3 -18 0
+-4 -19 0
+-5 -20 0
+-6 -21 0
+-7 -22 0
+-8 -23 0
+-9 -24 0
+-10 -25 0
+-11 -26 0
+-12 -27 0
+-13 -28 0
+-14 -29 0
+-15 -30 0
diff --git a/examples/php43.cnf b/examples/php43.cnf
new file mode 100644
index 0000000..2c544d2
--- /dev/null
+++ b/examples/php43.cnf
@@ -0,0 +1,24 @@
+c pigeonhole PHP(4,3): 4 pigeons, 3 holes, UNSAT
+p cnf 12 22
+1 2 3 0
+4 5 6 0
+7 8 9 0
+10 11 12 0
+-1 -4 0
+-1 -7 0
+-1 -10 0
+-4 -7 0
+-4 -10 0
+-7 -10 0
+-2 -5 0
+-2 -8 0
+-2 -11 0
+-5 -8 0
+-5 -11 0
+-8 -11 0
+-3 -6 0
+-3 -9 0
+-3 -12 0
+-6 -9 0
+-6 -12 0
+-9 -12 0
diff --git a/examples/php65.cnf b/examples/php65.cnf
new file mode 100644
index 0000000..58fdf5b
--- /dev/null
+++ b/examples/php65.cnf
@@ -0,0 +1,83 @@
+c pigeonhole PHP(6,5), UNSAT
+p cnf 30 81
+1 2 3 4 5 0
+6 7 8 9 10 0
+11 12 13 14 15 0
+16 17 18 19 20 0
+21 22 23 24 25 0
+26 27 28 29 30 0
+-1 -6 0
+-1 -11 0
+-1 -16 0
+-1 -21 0
+-1 -26 0
+-6 -11 0
+-6 -16 0
+-6 -21 0
+-6 -26 0
+-11 -16 0
+-11 -21 0
+-11 -26 0
+-16 -21 0
+-16 -26 0
+-21 -26 0
+-2 -7 0
+-2 -12 0
+-2 -17 0
+-2 -22 0
+-2 -27 0
+-7 -12 0
+-7 -17 0
+-7 -22 0
+-7 -27 0
+-12 -17 0
+-12 -22 0
+-12 -27 0
+-17 -22 0
+-17 -27 0
+-22 -27 0
+-3 -8 0
+-3 -13 0
+-3 -18 0
+-3 -23 0
+-3 -28 0
+-8 -13 0
+-8 -18 0
+-8 -23 0
+-8 -28 0
+-13 -18 0
+-13 -23 0
+-13 -28 0
+-18 -23 0
+-18 -28 0
+-23 -28 0
+-4 -9 0
+-4 -14 0
+-4 -19 0
+-4 -24 0
+-4 -29 0
+-9 -14 0
+-9 -19 0
+-9 -24 0
+-9 -29 0
+-14 -19 0
+-14 -24 0
+-14 -29 0
+-19 -24 0
+-19 -29 0
+-24 -29 0
+-5 -10 0
+-5 -15 0
+-5 -20 0
+-5 -25 0
+-5 -30 0
+-10 -15 0
+-10 -20 0
+-10 -25 0
+-10 -30 0
+-15 -20 0
+-15 -25 0
+-15 -30 0
+-20 -25 0
+-20 -30 0
+-25 -30 0
diff --git a/examples/queens8.cnf b/examples/queens8.cnf
new file mode 100644
index 0000000..d9e4df2
--- /dev/null
+++ b/examples/queens8.cnf
@@ -0,0 +1,738 @@
+c 8-queens placement, SAT
+p cnf 64 736
+1 2 3 4 5 6 7 8 0
+-1 -2 0
+-1 -3 0
+-1 -4 0
+-1 -5 0
+-1 -6 0
+-1 -7 0
+-1 -8 0
+-2 -3 0
+-2 -4 0
+-2 -5 0
+-2 -6 0
+-2 -7 0
+-2 -8 0
+-3 -4 0
+-3 -5 0
+-3 -6 0
+-3 -7 0
+-3 -8 0
+-4 -5 0
+-4 -6 0
+-4 -7 0
+-4 -8 0
+-5 -6 0
+-5 -7 0
+-5 -8 0
+-6 -7 0
+-6 -8 0
+-7 -8 0
+9 10 11 12 13 14 15 16 0
+-9 -10 0
+-9 -11 0
+-9 -12 0
+-9 -13 0
+-9 -14 0
+-9 -15 0
+-9 -16 0
+-10 -11 0
+-10 -12 0
+-10 -13 0
+-10 -14 0
+-10 -15 0
+-10 -16 0
+-11 -12 0
+-11 -13 0
+-11 -14 0
+-11 -15 0
+-11 -16 0
+-12 -13 0
+-12 -14 0
+-12 -15 0
+-12 -16 0
+-13 -14 0
+-13 -15 0
+-13 -16 0
+-14 -15 0
+-14 -16 0
+-15 -16 0
+17 18 19 20 21 22 23 24 0
+-17 -18 0
+-17 -19 0
+-17 -20 0
+-17 -21 0
+-17 -22 0
+-17 -23 0
+-17 -24 0
+-18 -19 0
+-18 -20 0
+-18 -21 0
+-18 -22 0
+-18 -23 0
+-18 -24 0
+-19 -20 0
+-19 -21 0
+-19 -22 0
+-19 -23 0
+-19 -24 0
+-20 -21 0
+-20 -22 0
+-20 -23 0
+-20 -24 0
+-21 -22 0
+-21 -23 0
+-21 -24 0
+-22 -23 0
+-22 -24 0
+-23 -24 0
+25 26 27 28 29 30 31 32 0
+-25 -26 0
+-25 -27 0
+-25 -28 0
+-25 -29 0
+-25 -30 0
+-25 -31 0
+-25 -32 0
+-26 -27 0
+-26 -28 0
+-26 -29 0
+-26 -30 0
+-26 -31 0
+-26 -32 0
+-27 -28 0
+-27 -29 0
+-27 -30 0
+-27 -31 0
+-27 -32 0
+-28 -29 0
+-28 -30 0
+-28 -31 0
+-28 -32 0
+-29 -30 0
+-29 -31 0
+-29 -32 0
+-30 -31 0
+-30 -32 0
+-31 -32 0
+33 34 35 36 37 38 39 40 0
+-33 -34 0
+-33 -35 0
+-33 -36 0
+-33 -37 0
+-33 -38 0
+-33 -39 0
+-33 -40 0
+-34 -35 0
+-34 -36 0
+-34 -37 0
+-34 -38 0
+-34 -39 0
+-34 -40 0
+-35 -36 0
+-35 -37 0
+-35 -38 0
+-35 -39 0
+-35 -40 0
+-36 -37 0
+-36 -38 0
+-36 -39 0
+-36 -40 0
+-37 -38 0
+-37 -39 0
+-37 -40 0
+-38 -39 0
+-38 -40 0
+-39 -40 0
+41 42 43 44 45 46 47 48 0
+-41 -42 0
+-41 -43 0
+-41 -44 0
+-41 -45 0
+-41 -46 0
+-41 -47 0
+-41 -48 0
+-42 -43 0
+-42 -44 0
+-42 -45 0
+-42 -46 0
+-42 -47 0
+-42 -48 0
+-43 -44 0
+-43 -45 0
+-43 -46 0
+-43 -47 0
+-43 -48 0
+-44 -45 0
+-44 -46 0
+-44 -47 0
+-44 -48 0
+-45 -46 0
+-45 -47 0
+-45 -48 0
+-46 -47 0
+-46 -48 0
+-47 -48 0
+49 50 51 52 53 54 55 56 0
+-49 -50 0
+-49 -51 0
+-49 -52 0
+-49 -53 0
+-49 -54 0
+-49 -55 0
+-49 -56 0
+-50 -51 0
+-50 -52 0
+-50 -53 0
+-50 -54 0
+-50 -55 0
+-50 -56 0
+-51 -52 0
+-51 -53 0
+-51 -54 0
+-51 -55 0
+-51 -56 0
+-52 -53 0
+-52 -54 0
+-52 -55 0
+-52 -56 0
+-53 -54 0
+-53 -55 0
+-53 -56 0
+-54 -55 0
+-54 -56 0
+-55 -56 0
+57 58 59 60 61 62 63 64 0
+-57 -58 0
+-57 -59 0
+-57 -60 0
+-57 -61 0
+-57 -62 0
+-57 -63 0
+-57 -64 0
+-58 -59 0
+-58 -60 0
+-58 -61 0
+-58 -62 0
+-58 -63 0
+-58 -64 0
+-59 -60 0
+-59 -61 0
+-59 -62 0
+-59 -63 0
+-59 -64 0
+-60 -61 0
+-60 -62 0
+-60 -63 0
+-60 -64 0
+-61 -62 0
+-61 -63 0
+-61 -64 0
+-62 -63 0
+-62 -64 0
+-63 -64 0
+-1 -9 0
+-1 -17 0
+-1 -25 0
+-1 -33 0
+-1 -41 0
+-1 -49 0
+-1 -57 0
+-9 -17 0
+-9 -25 0
+-9 -33 0
+-9 -41 0
+-9 -49 0
+-9 -57 0
+-17 -25 0
+-17 -33 0
+-17 -41 0
+-17 -49 0
+-17 -57 0
+-25 -33 0
+-25 -41 0
+-25 -49 0
+-25 -57 0
+-33 -41 0
+-33 -49 0
+-33 -57 0
+-41 -49 0
+-41 -57 0
+-49 -57 0
+-2 -10 0
+-2 -18 0
+-2 -26 0
+-2 -34 0
+-2 -42 0
+-2 -50 0
+-2 -58 0
+-10 -18 0
+-10 -26 0
+-10 -34 0
+-10 -42 0
+-10 -50 0
+-10 -58 0
+-18 -26 0
+-18 -34 0
+-18 -42 0
+-18 -50 0
+-18 -58 0
+-26 -34 0
+-26 -42 0
+-26 -50 0
+-26 -58 0
+-34 -42 0
+-34 -50 0
+-34 -58 0
+-42 -50 0
+-42 -58 0
+-50 -58 0
+-3 -11 0
+-3 -19 0
+-3 -27 0
+-3 -35 0
+-3 -43 0
+-3 -51 0
+-3 -59 0
+-11 -19 0
+-11 -27 0
+-11 -35 0
+-11 -43 0
+-11 -51 0
+-11 -59 0
+-19 -27 0
+-19 -35 0
+-19 -43 0
+-19 -51 0
+-19 -59 0
+-27 -35 0
+-27 -43 0
+-27 -51 0
+-27 -59 0
+-35 -43 0
+-35 -51 0
+-35 -59 0
+-43 -51 0
+-43 -59 0
+-51 -59 0
+-4 -12 0
+-4 -20 0
+-4 -28 0
+-4 -36 0
+-4 -44 0
+-4 -52 0
+-4 -60 0
+-12 -20 0
+-12 -28 0
+-12 -36 0
+-12 -44 0
+-12 -52 0
+-12 -60 0
+-20 -28 0
+-20 -36 0
+-20 -44 0
+-20 -52 0
+-20 -60 0
+-28 -36 0
+-28 -44 0
+-28 -52 0
+-28 -60 0
+-36 -44 0
+-36 -52 0
+-36 -60 0
+-44 -52 0
+-44 -60 0
+-52 -60 0
+-5 -13 0
+-5 -21 0
+-5 -29 0
+-5 -37 0
+-5 -45 0
+-5 -53 0
+-5 -61 0
+-13 -21 0
+-13 -29 0
+-13 -37 0
+-13 -45 0
+-13 -53 0
+-13 -61 0
+-21 -29 0
+-21 -37 0
+-21 -45 0
+-21 -53 0
+-21 -61 0
+-29 -37 0
+-29 -45 0
+-29 -53 0
+-29 -61 0
+-37 -45 0
+-37 -53 0
+-37 -61 0
+-45 -53 0
+-45 -61 0
+-53 -61 0
+-6 -14 0
+-6 -22 0
+-6 -30 0
+-6 -38 0
+-6 -46 0
+-6 -54 0
+-6 -62 0
+-14 -22 0
+-14 -30 0
+-14 -38 0
+-14 -46 0
+-14 -54 0
+-14 -62 0
+-22 -30 0
+-22 -38 0
+-22 -46 0
+-22 -54 0
+-22 -62 0
+-30 -38 0
+-30 -46 0
+-30 -54 0
+-30 -62 0
+-38 -46 0
+-38 -54 0
+-38 -62 0
+-46 -54 0
+-46 -62 0
+-54 -62 0
+-7 -15 0
+-7 -23 0
+-7 -31 0
+-7 -39 0
+-7 -47 0
+-7 -55 0
+-7 -63 0
+-15 -23 0
+-15 -31 0
+-15 -39 0
+-15 -47 0
+-15 -55 0
+-15 -63 0
+-23 -31 0
+-23 -39 0
+-23 -47 0
+-23 -55 0
+-23 -63 0
+-31 -39 0
+-31 -47 0
+-31 -55 0
+-31 -63 0
+-39 -47 0
+-39 -55 0
+-39 -63 0
+-47 -55 0
+-47 -63 0
+-55 -63 0
+-8 -16 0
+-8 -24 0
+-8 -32 0
+-8 -40 0
+-8 -48 0
+-8 -56 0
+-8 -64 0
+-16 -24 0
+-16 -32 0
+-16 -40 0
+-16 -48 0
+-16 -56 0
+-16 -64 0
+-24 -32 0
+-24 -40 0
+-24 -48 0
+-24 -56 0
+-24 -64 0
+-32 -40 0
+-32 -48 0
+-32 -56 0
+-32 -64 0
+-40 -48 0
+-40 -56 0
+-40 -64 0
+-48 -56 0
+-48 -64 0
+-56 -64 0
+-7 -16 0
+-6 -15 0
+-6 -24 0
+-15 -24 0
+-5 -14 0
+-5 -23 0
+-5 -32 0
+-14 -23 0
+-14 -32 0
+-23 -32 0
+-4 -13 0
+-4 -22 0
+-4 -31 0
+-4 -40 0
+-13 -22 0
+-13 -31 0
+-13 -40 0
+-22 -31 0
+-22 -40 0
+-31 -40 0
+-3 -12 0
+-3 -21 0
+-3 -30 0
+-3 -39 0
+-3 -48 0
+-12 -21 0
+-12 -30 0
+-12 -39 0
+-12 -48 0
+-21 -30 0
+-21 -39 0
+-21 -48 0
+-30 -39 0
+-30 -48 0
+-39 -48 0
+-2 -11 0
+-2 -20 0
+-2 -29 0
+-2 -38 0
+-2 -47 0
+-2 -56 0
+-11 -20 0
+-11 -29 0
+-11 -38 0
+-11 -47 0
+-11 -56 0
+-20 -29 0
+-20 -38 0
+-20 -47 0
+-20 -56 0
+-29 -38 0
+-29 -47 0
+-29 -56 0
+-38 -47 0
+-38 -56 0
+-47 -56 0
+-1 -10 0
+-1 -19 0
+-1 -28 0
+-1 -37 0
+-1 -46 0
+-1 -55 0
+-1 -64 0
+-10 -19 0
+-10 -28 0
+-10 -37 0
+-10 -46 0
+-10 -55 0
+-10 -64 0
+-19 -28 0
+-19 -37 0
+-19 -46 0
+-19 -55 0
+-19 -64 0
+-28 -37 0
+-28 -46 0
+-28 -55 0
+-28 -64 0
+-37 -46 0
+-37 -55 0
+-37 -64 0
+-46 -55 0
+-46 -64 0
+-55 -64 0
+-9 -18 0
+-9 -27 0
+-9 -36 0
+-9 -45 0
+-9 -54 0
+-9 -63 0
+-18 -27 0
+-18 -36 0
+-18 -45 0
+-18 -54 0
+-18 -63 0
+-27 -36 0
+-27 -45 0
+-27 -54 0
+-27 -63 0
+-36 -45 0
+-36 -54 0
+-36 -63 0
+-45 -54 0
+-45 -63 0
+-54 -63 0
+-17 -26 0
+-17 -35 0
+-17 -44 0
+-17 -53 0
+-17 -62 0
+-26 -35 0
+-26 -44 0
+-26 -53 0
+-26 -62 0
+-35 -44 0
+-35 -53 0
+-35 -62 0
+-44 -53 0
+-44 -62 0
+-53 -62 0
+-25 -34 0
+-25 -43 0
+-25 -52 0
+-25 -61 0
+-34 -43 0
+-34 -52 0
+-34 -61 0
+-43 -52 0
+-43 -61 0
+-52 -61 0
+-33 -42 0
+-33 -51 0
+-33 -60 0
+-42 -51 0
+-42 -60 0
+-51 -60 0
+-41 -50 0
+-41 -59 0
+-50 -59 0
+-49 -58 0
+-2 -9 0
+-3 -10 0
+-3 -17 0
+-10 -17 0
+-4 -11 0
+-4 -18 0
+-4 -25 0
+-11 -18 0
+-11 -25 0
+-18 -25 0
+-5 -12 0
+-5 -19 0
+-5 -26 0
+-5 -33 0
+-12 -19 0
+-12 -26 0
+-12 -33 0
+-19 -26 0
+-19 -33 0
+-26 -33 0
+-6 -13 0
+-6 -20 0
+-6 -27 0
+-6 -34 0
+-6 -41 0
+-13 -20 0
+-13 -27 0
+-13 -34 0
+-13 -41 0
+-20 -27 0
+-20 -34 0
+-20 -41 0
+-27 -34 0
+-27 -41 0
+-34 -41 0
+-7 -14 0
+-7 -21 0
+-7 -28 0
+-7 -35 0
+-7 -42 0
+-7 -49 0
+-14 -21 0
+-14 -28 0
+-14 -35 0
+-14 -42 0
+-14 -49 0
+-21 -28 0
+-21 -35 0
+-21 -42 0
+-21 -49 0
+-28 -35 0
+-28 -42 0
+-28 -49 0
+-35 -42 0
+-35 -49 0
+-42 -49 0
+-8 -15 0
+-8 -22 0
+-8 -29 0
+-8 -36 0
+-8 -43 0
+-8 -50 0
+-8 -57 0
+-15 -22 0
+-15 -29 0
+-15 -36 0
+-15 -43 0
+-15 -50 0
+-15 -57 0
+-22 -29 0
+-22 -36 0
+-22 -43 0
+-22 -50 0
+-22 -57 0
+-29 -36 0
+-29 -43 0
+-29 -50 0
+-29 -57 0
+-36 -43 0
+-36 -50 0
+-36 -57 0
+-43 -50 0
+-43 -57 0
+-50 -57 0
+-16 -23 0
+-16 -30 0
+-16 -37 0
+-16 -44 0
+-16 -51 0
+-16 -58 0
+-23 -30 0
+-23 -37 0
+-23 -44 0
+-23 -51 0
+-23 -58 0
+-30 -37 0
+-30 -44 0
+-30 -51 0
+-30 -58 0
+-37 -44 0
+-37 -51 0
+-37 -58 0
+-44 -51 0
+-44 -58 0
+-51 -58 0
+-24 -31 0
+-24 -38 0
+-24 -45 0
+-24 -52 0
+-24 -59 0
+-31 -38 0
+-31 -45 0
+-31 -52 0
+-31 -59 0
+-38 -45 0
+-38 -52 0
+-38 -59 0
+-45 -52 0
+-45 -59 0
+-52 -59 0
+-32 -39 0
+-32 -46 0
+-32 -53 0
+-32 -60 0
+-39 -46 0
+-39 -53 0
+-39 -60 0
+-46 -53 0
+-46 -60 0
+-53 -60 0
+-40 -47 0
+-40 -54 0
+-40 -61 0
+-47 -54 0
+-47 -61 0
+-54 -61 0
+-48 -55 0
+-48 -62 0
+-55 -62 0
+-56 -63 0
diff --git a/examples/sat.cnf b/examples/sat.cnf
new file mode 100644
index 0000000..a230c25
--- /dev/null
+++ b/examples/sat.cnf
@@ -0,0 +1,7 @@
+c sample satisfiable formula
+c (x1 or x2 or -x3) and (-x1 or x3) and (-x2 or x3) and (x1 or x2)
+p cnf 3 4
+1 2 -3 0
+-1 3 0
+-2 3 0
+1 2 0
diff --git a/examples/unsat.cnf b/examples/unsat.cnf
new file mode 100644
index 0000000..48d50be
--- /dev/null
+++ b/examples/unsat.cnf
@@ -0,0 +1,5 @@
+c sample unsatisfiable formula
+c (x1) and (-x1)
+p cnf 1 2
+1 0
+-1 0