SAT-based KenKen Solver

Inspired by the SAT-based Sudoku solver by Tjark Weber and the corresponding Python implementation, I coded up a quick SAT-based KenKen solver.

The ideas in the KenKen solver are pretty similar to the Sudoku solver. In particular, we reuse the framework of using a boolean variable to represent
each possible digit in each cell and all of the clauses which correspond to the following rules:

  • At least one digit must be present in a cell
  • Two or more digits may not be present in a cell
  • The same digit may not appear more than once in any row
  • The same digit may not appear more than once in any column

To satisfy the mathematical expressions, we generate all list of all possible ways each “cage” can be filled. This is most naturally expressed in disjunctive normal form:

(cell1 has value v1 AND cell2 has value v2 AND ...)
OR (cell1 is value w1 AND cell2 has value w2 AND ...)
OR ...

This can be easily and efficiently transformed into a equisatisfiable conjunctive normal form by adding a few auxiliary variables.

The SAT-based solver is reasonably fast. For example, on my laptop it can solve a 6-by-6 KenKen problem in about 23 ms. On a big a 9-by-9 problem it takes about 328 ms which is a factor of 5 or so slower than the NekNek solver (which takes about 65 ms).

Story of a bug in Ubuntu

I just came across this lovely writeup of a particularly annoying bug I helped squash in Ubuntu 12.04. The bug caused applications like evince and eog to load incredibly slowly, taking almost a full minute to open a PDF. It turned out to have a relatively banal cause — an initialization procedure didn’t immediately signal its failure and instead the library would wait a full 5 seconds for the initialization to finish before giving up.

Thanks for the writeup, Emanuele Rocca. I think this shows the power of open source software. An obscure bug affecting only a handful of people can still get fixed, even without much help from the original developers.

Changing screen resolution in RealVNC

These days I do most of my work in a RealVNC session on a remote Ubuntu workstation. This provides me with a consistent environment, regardless of whether I’m at work, a coffee shop, or at home. One major annoyance with the default configuration is that the screen resolution cannot be changed after the virtual desktop is started.

The key to getting around this problem is to provide RealVNC with a complete list of screen resolutions you would like to have available when starting RealVNC. For example, my .vnc/config file contains

# Additional Resolutions
-randr 800x600,1024x768,1280x800,1280x960,1280x1024,1344x756,1680x1050,1920x1080,1920x1200,3360x1050,1024x700,1200x740,1600x1000,3200x1000,1680x1020,768x1024

After restarting RealVNC, you can easily change the screen resolution using the xrandr command. You can list screen resolutions by running xrandr:

$ xrandr
 SZ:    Pixels          Physical       Refresh
 0    800 x 600    ( 203mm x 152mm )   0
 1   1024 x 768    ( 260mm x 195mm )   0
 2   1280 x 800    ( 325mm x 203mm )   0
 3   1280 x 960    ( 325mm x 244mm )   0
 4   1280 x 1024   ( 325mm x 260mm )   0
 5   1344 x 756    ( 341mm x 192mm )   0
 6   1680 x 1050   ( 427mm x 267mm )   0
*7   1920 x 1080   ( 488mm x 274mm )  *0
 8   1920 x 1200   ( 488mm x 305mm )   0
 9   3360 x 1050   ( 853mm x 267mm )   0
 10  1024 x 700    ( 260mm x 178mm )   0
 11  1200 x 740    ( 305mm x 188mm )   0
 12  1600 x 1000   ( 406mm x 254mm )   0
 13  3200 x 1000   ( 813mm x 254mm )   0
 14  1680 x 1020   ( 427mm x 259mm )   0
 15   768 x 1024   ( 195mm x 260mm )   0
Current rotation - normal
Current reflection - none
Rotations possible - normal
Reflections possible - none

To switch to a different resolution just run xrandr -s <resolution>, where the resolution is either the item number, like 12, or resolution, like 1600x1000.

Afterwards, especially in recent versions of Ubuntu (12.04 and later), you may find that the background Nautilus desktop didn’t get the memo that the screen resolution was changed. To work around this, it’s often easiest to quit and restart Nautilus:

$ nautilus -q; sleep 1; nautilus -n > /dev/null 2>&1 & disown %

If you find yourself doing this a lot, as I did, you may want to consider writing a little script to automate the task. I named my script xres and have posted the source as a gist.

RealVNC on Ubuntu 13.04 Raring Ringtail

I just spent a few hours getting the free version RealVNC working in Ubuntu 13.04 Raring Ringtail (Beta 2). Here are the steps that I needed to take:

  1. Disable the X Server Render extension. Copy /etc/vnc/config to /etc/vnc/config.custom and add
    -extension RENDER
  2. Create a custom xstartup file. Copy /etc/vnc/xstartup to /etc/vnc/xstartup.custom and make the following changes:
    • Remove the line
      [ -x /etc/vnc/xstartup.custom ] && exec /etc/vnc/xstartup.custom
    • Add "gnome-fallback" to the list of valid sessions by replacing
      for SESSION in "ubuntu-2d" "2d-gnome"; do


      for SESSION in "ubuntu-2d" "2d-gnome" "gnome-fallback"; do
    • Add to the top of the file:
      unset XDG_RUNTIME_DIR

I found it necessary to unset XDG_RUNTIME_DIR because I could not figure out a way to guarantee the directory it points to actually exists. When the directory did not exist I experienced 100% CPU utilization bugs in indicator-datetime-service and gnome-settings-daemon.

Briefly, the XDG_RUNTIME_DIR variable and directory that it points to are managed by a PAM module in libpam-xdg-support. When jsmith logs in over SSH, the PAM module creates a directory /run/users/jsmith and increments a session count stored in /run/users/.jsmith.lock. When jsmith later logs out, the session count is decremented. When the session count reaches zero the directory is deleted. Since RealVNC does not appear to use the PAM session machinery, there is no way to guarantee that the session count remains positive if only a VNC session is active.

A data descriptor for __doc__

In Python, suppose you want to implement a class which has a dynamically generated docstring. The easiest way to do this would be to use the @property decorator for the __doc__ attribute. (You also need your class to be a “new-style” class, i.e., inherit from object). For example:

class A(object):
    """Docstring for class."""
    def __init__(self, x):
        self.x = x
    def __doc__(self):
        return "My value of x is %s." % self.x

This gives the desired result:

>>> a = A(10)
>>> print(a.__doc__)
My value of x is 10.

But hides the docstring for the class A:

>>> A.__doc__
<property at 0x2083db8>

Read on to see how we can fix this. Continue reading A data descriptor for __doc__

Instance Methods & Cython Functions

One of the great features of Python is the ability to define methods outside of classes. For example, we can define a function which increments the attribute x and add it to a Point class:

def incx(self):
    self.x += 1

class Point(object):
    def __init__(self, x): self.x = x
    incx = incx

We can then create a point at the origin and increment x:

In [2]: p = Point(0)

In [3]: p.incx()

In [4]: print p.x

The same code which defines Point continues to work if we move incx to another file, say, and import it using from demo import incx.

But if we were to put incx in demo.pyx and compile it (using python build_ext --inplace), we get a strange error when running our simple test:

$ python
Traceback (most recent call last):
  File "", line 10, in <module>
TypeError: incx() takes exactly one argument (0 given)

Read on to learn about instance methods and see how I fixed this.
Continue reading Instance Methods & Cython Functions

True division in IPython

As Python transitions from version 2 to version 3, the meaning of the division operator on integers is changing:

Python 2.x Python 3.x
$ python2.7
Python 2.7.2+ (...)
>>> 1/2
$ python3.2
Python 3.2.2 (...)
>>> 1/2

In this post, we’ll discuss how to configure the behavior of the division operator in Python 2.7 and IPython to behave like the Python 3.x counterpart.

Continue reading True division in IPython

IPython Qt Console and printf

The recent 0.11 release of IPython includes a Qt-based console which offers an improved experience compared to running IPython in a terminal. In particular, the console feels like a terminal but offers multi-line editing, syntax highlighting, graphical tooltips, and inline plot figures.

But when I tried to run an existing script in the new IPython Qt Console, the usual overly verbose set of diagnostic messages did not appear! The symtoms were:

  • Regular print statements in Python worked fine.
  • printf statements in C-code wrapped with Boost.Python did not appear.

Read on to see a solution. Continue reading IPython Qt Console and printf

FILE* and Boost.Python

One great feature of Boost.Python is the ability to write custom converters from Python types to C++ arguments. Most Boost.Python documentation, including the incredibly helpful post by misspent, show you how to write “rvalue” converters (e.g., pass-by-value or pass-by-const-reference).

However if you need to wrap a function which takes a FILE* argument the previous approach will not prove fruitful. But Boost.Python is clearly capable of handling a similar situation, namely the implicit conversion from a Python string type to a char* type. Since the conversion from the internal PyObject* to char* is likely to be done with the PyString_AsString function, I went off in search of that code.

Continue reading FILE* and Boost.Python