CNF shuffling

plot.py

#!/usr/bin/env python
import sys
import re
import matplotlib.pyplot as plt
import matplotlib.cm as cm
from numpy import array
from matplotlib import animation

data = {}

for line in sys.stdin:
    r = re.match('^(\d+)\.(\d+).* (\d+\.\d+) seconds', line)
    (c, x, y) = r.groups()
    c = int(c)
    if not data.has_key(c): data[c] = {}
    data[c][x] = float(y)

def data_sets((c,d)):
    ys = d.items()
    ys.sort()
    ys = array(map(lambda (_,y): y, ys))
    ys = ys / max(ys)
    xs = range(1, 1+len(ys))
    cl = cm.Set1(float(c)/len(ys))
    return (cl,xs,ys)

points = map(data_sets, data.items())
fig = plt.figure()

def loop(i):
    plt.cla()
    (col, xs, ys) = points[i]
    plt.scatter(xs, ys, c='k', marker='+', s=500)
    for col, xs, ys in points:
        plt.scatter(xs, ys, c=col, s=200, alpha=0.5)

anim = animation.FuncAnimation(fig, loop, frames=len(points))
anim.save('scatter.gif', writer='imagemagick', fps=2)

test.sh

#!/bin/bash

# http://zelych.livejournal.com/22383.html

IFS=" " read -a h <<< `head -n -1 $1`
rs=()
for i in {1..10} ; do
  rs[$i]=$(($RANDOM%1024))
done

for i in {1..10} ; do
  tail -n +2 $1 | sort -R > $i.shuffle
  for j in {1..10} ; do
    r=${rs[$j]}
    f=$i.$r.cnf
    # header
    echo ${h[0]} ${h[1]} ${h[2]} $((${h[3]} + 10)) > $f
    # fixed vars
    for bit in {0..9} ; do
      val=$((2**bit))
      echo $(( -1 ** (($val & $r) / $val) * ($bit+1) )) 0 >> $f
    done
    # shuffled clauses
    cat $i.shuffle >> $f
    echo $f
    ../lingeling/binary/lingeling $f > $f.log
  done
done

grep 'seconds,' *log | ./plot.py