SAT-based BGA escape-routing generator; "satescapetion", maybe?

This is proof-of-principle code, and I claim it has successfully proved its
principle. You know the old saying about software development, "plan to throw
one away, you will anyway". Well, I already threw some away, and at least
half of the current code needs desperately to be refactored. Let's go for
"somewhat useful" first, then see about "featureful and maintainable".

Right now it can handle some Xilinx BGA packages,
power and differential pairs only, horizontal escapes only (actually a
good plan for the xc7a200t-ffg1156). Output is an old-style .pcb file.
It isn't likely to pass meaningful design rules until it can remove copper
from some layers in a pad stack. It follows the two-traces-between-balls
strategy for 1.0 mm packages shown in Xilinx's UG1099. Note that the sample
breakouts shown in that UG seem not to pay attention to signal pairs.

Implemented in less than 500 lines of Python (2 or 3, doesn't matter),
using minisat for the SAT solver.

Tested on
xc7a100tftg256pkg.txt
xc7a100tfgg484pkg.txt
xc7a200tfbg676pkg.txt
xc7a200tffg1156pkg.txt
downloaded directly from Xilinx's servers. The Makefile has rules
that will download them for you, if you don't already have a copy.

Count of left- and right-half pairs:
routed out on each layer
total stuck top 1 2 3 4
xc7a100t-ftg256 L 41 2 14 15 9 1 -
xc7a100t-ftg256 R 40 1 15 17 7 - -
xc7a100t-fgg484 L 54 0 19 18 10 6 1
xc7a100t-fgg484 R 83 0 18 24 24 17 -
xc7a200t-fbg676 L 72 1 24 28 19 - -
xc7a200t-fbg676 R 120 0 23 28 28 26 14
xc7a200t-ffg1156 L 120 0 27 30 29 28 6
xc7a200t-ffg1156 R 120 1 26 30 30 28 5

.. where "stuck" means they got trapped on the top layer without an escape.
The routing is purely algorithmic; there is no hand-tuning for any of these
files in particular. My ancient laptop can route all four full packages
in about 16 seconds total.

To do, besides major refactoring:
- maximize decoupling cap stripes
- allow controlling the balance between horizontal and vertical escapes
- consider (and test) using python-minisat