Apparently simple, but really rather deep

Computing pioneer Maurice Wilkes, in a letter to Tony Hoare from August 1981:

. . . loop invariants . . . The idea is apparently simple, but really rather deep.  Once you have grasped it fully – and I must confess that, although Floyd was very patient with me, it was some time before I did this – you will never look at the subject in the same way again.

Quoted in C. B. Jones, The Early Search for Tractable Ways of Reasoning about Programs, IEEE Annals of the History of Computing, Vol 25, No 2, pp26-49, 2003

A Sudoku Solver in Alloy

A couple of days ago I got stuck doing the sudoku in the Evening Standard.  Normally I just work my way through these puzzles by lightly pencilling in all the possible numbers and then systematically eliminating and erasing possibilities until only one remains for each square.  However, this time, I reached a point from which I just could not see any way to progress.  I would normally have taken this as a sign that I had made a mistake, and erased everything and started again.  But, instead I decided to write an Alloy model to solve sudoku once and for all.  In that way I hoped to cure myself of wasting time on these pointless little puzzles.

/* Sudoku.als - A Sudoku Solver on Alloy */


abstract sig Cols {}
one sig c1, c2, c3, c4, c5, c6, c7, c8, c9 extends Cols {}


abstract sig Rows {}
one sig r1, r2, r3, r4, r5, r6, r7, r8, r9 extends Rows {}


abstract sig Boxes {}
one sig b11, b12, b13, b21, b22, b23, b31, b32, b33 extends Boxes {}


abstract sig Nums {}
one sig n1, n2, n3, n4, n5, n6, n7, n8, n9 extends Nums {}


abstract sig Cells {
	col : Cols,
	row : Rows,
	box : Boxes,
	num : Nums
}

one sig c11, c12, c13, c14, c15, c16, c17, c18, c19 extends Cells {}
one sig c21, c22, c23, c24, c25, c26, c27, c28, c29 extends Cells {}
one sig c31, c32, c33, c34, c35, c36, c37, c38, c39 extends Cells {}
one sig c41, c42, c43, c44, c45, c46, c47, c48, c49 extends Cells {}
one sig c51, c52, c53, c54, c55, c56, c57, c58, c59 extends Cells {}
one sig c61, c62, c63, c64, c65, c66, c67, c68, c69 extends Cells {}
one sig c71, c72, c73, c74, c75, c76, c77, c78, c79 extends Cells {}
one sig c81, c82, c83, c84, c85, c86, c87, c88, c89 extends Cells {}
one sig c91, c92, c93, c94, c95, c96, c97, c98, c99 extends Cells {}

fact Col_structure {
	(c11+c21+c31+c41+c51+c61+c71+c81+c91).col in c1 and
	(c12+c22+c32+c42+c52+c62+c72+c82+c92).col in c2 and
	(c13+c23+c33+c43+c53+c63+c73+c83+c93).col in c3 and
	(c14+c24+c34+c44+c54+c64+c74+c84+c94).col in c4 and
	(c15+c25+c35+c45+c55+c65+c75+c85+c95).col in c5 and
	(c16+c26+c36+c46+c56+c66+c76+c86+c96).col in c6 and
	(c17+c27+c37+c47+c57+c67+c77+c87+c97).col in c7 and
	(c18+c28+c38+c48+c58+c68+c78+c88+c98).col in c8 and
	(c19+c29+c39+c49+c59+c69+c79+c89+c99).col in c9
}

fact Row_structure {
	(c11+c12+c13+c14+c15+c16+c17+c18+c19).row in r1 and
	(c21+c22+c23+c24+c25+c26+c27+c28+c29).row in r2 and
	(c31+c32+c33+c34+c35+c36+c37+c38+c39).row in r3 and
	(c41+c42+c43+c44+c45+c46+c47+c48+c49).row in r4 and
	(c51+c52+c53+c54+c55+c56+c57+c58+c59).row in r5 and
	(c61+c62+c63+c64+c65+c66+c67+c68+c69).row in r6 and
	(c71+c72+c73+c74+c75+c76+c77+c78+c79).row in r7 and
	(c81+c82+c83+c84+c85+c86+c87+c88+c89).row in r8 and
	(c91+c92+c93+c94+c95+c96+c97+c98+c99).row in r9
}

fact Box_structure {
	(c11+c12+c13+c21+c22+c23+c31+c32+c33).box in b11 and
	(c14+c15+c16+c24+c25+c26+c34+c35+c36).box in b12 and
	(c17+c18+c19+c27+c28+c29+c37+c38+c39).box in b13 and
	(c41+c42+c43+c51+c52+c53+c61+c62+c63).box in b21 and
	(c44+c45+c46+c54+c55+c56+c64+c65+c66).box in b22 and
	(c47+c48+c49+c57+c58+c59+c67+c68+c69).box in b23 and
	(c71+c72+c73+c81+c82+c83+c91+c92+c93).box in b31 and
	(c74+c75+c76+c84+c85+c86+c94+c95+c96).box in b32 and
	(c77+c78+c79+c87+c88+c89+c97+c98+c99).box in b33
}


fact Rules_of_the_game {
	no disj c1, c2 : Cells |
		c1.num = c2.num and
		(c1.col = c2.col or c1.row = c2.row or c1.box = c2.box)
}


pred EveningStandard20120404 {
	/*
	+-------+-------+-------+
	| _ 7 _ | 5 _ 8 | _ _ _ |
	| _ 9 _ | _ _ _ | _ _ _ |
	| 3 _ 2 | 1 _ _ | _ 9 _ |
	+-------+-------+-------+
	| 7 _ 6 | _ _ _ | _ _ 8 |
	| _ _ _ | 4 _ 5 | _ _ _ |
	| 5 _ _ | _ _ _ | 9 _ 4 |
	+-------+-------+-------+
	| _ 3 _ | _ _ 2 | 5 _ 7 |
	| _ _ _ | _ _ _ | _ 2 _ |
	| _ _ _ | 6 _ 4 | _ 3 _ |
	+-------+-------+-------+
	*/
	c12.num in n7 and c14.num in n5 and c16.num in n8 and
	c22.num in n9 and
	c31.num in n3 and c33.num in n2 and c34.num in n1 and c38.num in n9 and
	c41.num in n7 and c43.num in n6 and c49.num in n8 and
	c54.num in n4 and c56.num in n5 and
	c61.num in n5 and c67.num in n9 and c69.num in n4 and
	c72.num in n3 and c76.num in n2 and c77.num in n5 and c79.num in n7 and
	c88.num in n2 and
	c94.num in n6 and c96.num in n4 and c98.num in n3
}


run {EveningStandard20120404} for 9 Cols, 9 Rows, 9 Boxes, 9 Nums, 81 Cells

	/*
	This gives the following solution, expressed as a predicate (see the Txt display):

	this/Cells<:num={
		c11$0->n6$0, c12$0->n7$0, c13$0->n1$0, c14$0->n5$0, c15$0->n9$0, c16$0->n8$0, c17$0->n2$0, c18$0->n4$0, c19$0->n3$0,
		c21$0->n4$0, c22$0->n9$0, c23$0->n5$0, c24$0->n7$0, c25$0->n2$0, c26$0->n3$0, c27$0->n1$0, c28$0->n8$0, c29$0->n6$0,
		c31$0->n3$0, c32$0->n8$0, c33$0->n2$0, c34$0->n1$0, c35$0->n4$0, c36$0->n6$0, c37$0->n7$0, c38$0->n9$0, c39$0->n5$0,
		c41$0->n7$0, c42$0->n4$0, c43$0->n6$0, c44$0->n2$0, c45$0->n1$0, c46$0->n9$0, c47$0->n3$0, c48$0->n5$0, c49$0->n8$0,
		c51$0->n9$0, c52$0->n1$0, c53$0->n8$0, c54$0->n4$0, c55$0->n3$0, c56$0->n5$0, c57$0->n6$0, c58$0->n7$0, c59$0->n2$0,
		c61$0->n5$0, c62$0->n2$0, c63$0->n3$0, c64$0->n8$0, c65$0->n6$0, c66$0->n7$0, c67$0->n9$0, c68$0->n1$0, c69$0->n4$0,
		c71$0->n1$0, c72$0->n3$0, c73$0->n4$0, c74$0->n9$0, c75$0->n8$0, c76$0->n2$0, c77$0->n5$0, c78$0->n6$0, c79$0->n7$0,
		c81$0->n8$0, c82$0->n6$0, c83$0->n7$0, c84$0->n3$0, c85$0->n5$0, c86$0->n1$0, c87$0->n4$0, c88$0->n2$0, c89$0->n9$0,
		c91$0->n2$0, c92$0->n5$0, c93$0->n9$0, c94$0->n6$0, c95$0->n7$0, c96$0->n4$0, c97$0->n8$0, c98$0->n3$0, c99$0->n1$0
	}
	Expressed as a diagram the solution is:
	+-------+-------+-------+
	| 6 7 1 | 5 9 8 | 2 4 3 |
	| 4 9 5 | 7 2 3 | 1 8 6 |
	| 3 8 2 | 1 4 6 | 7 9 5 |
	+-------+-------+-------+
	| 7 4 6 | 2 1 9 | 3 5 8 |
	| 9 1 8 | 4 3 5 | 6 7 2 |
	| 5 2 3 | 8 6 7 | 9 1 4 |
	+-------+-------+-------+
	| 1 3 4 | 9 8 2 | 5 6 7 |
	| 8 6 7 | 3 5 1 | 4 2 9 |
	| 2 5 9 | 6 7 4 | 8 3 1 |
	+-------+-------+-------+
	Finding this solution took 12s on a laptop with a 1.4GHz processor.
	No further solutions were found.
	*/

The definition of this/Cells in the last comment overflows the right margin, so I have also included a full copy of the source file here.

I used named atoms to represent not only the cells, rows, columns and boxes, but also the numbers that go in the cells.  It might seem more obvious to use integers  to represent the numbers but we do not need the full properties of integers (or of natural numbers).  All we need is to be able to test whether or not two numbers are the same, and for this named atoms are adequate.  Sudoku would still work if you had to fill the cells with letters, or even colours.

If I was writing a sudoku solver in a proper programming language I would certainly use integers instead of named atoms.  This would enable me to calculate the row, column and box structures, instead of manually enumerating them, which would make things less error-prone.

One thing that surprised me was the shortness of the Rules_of_the_game definition: just three lines.  Alloy is good at capturing the essence of a system in a very succinct expression.

 As you can see, I ran the model on the Evening Standard puzzle and it produced a solution.  I checked the solution manually and it was correct.  I got Alloy to look for further solutions and it couldn't find any, so the solution was unique.  I compared the solution with my attempt and I had not made any mistakes, but the solution gave no hint on how I could make progress from the position I had got to.  The model gave a solution but gave no insight as to how to get to that solution.  So the model didn't really solve my problem, which was that of finding the next move in a given position.  But I will leave that problem to the reader.  I might get round to looking at it some day.

Moving the BackupPC Data Directory to an external Hard Disk Drive

In Ubuntu 10.04 LTS the default install of BackupPC stores all the backups in the directory /var/lib/backuppc which is located on the main hard disk drive /dev/sda.  However, I wanted to store all my backups on an external USB hard disk drive /dev/sdb.  This post records what I had to do to get this to work.

Reformat the External Hard Disk

The external hard disk drive came with its disk preformatted as an NTFS file system. This file system does not support hard links which are critical for the efficient operation of BackupPC, so first we reformat the disk to EXT4 (a file system that does support hard links).

Display the partitions (I use parted rather than fdisk because its display is a bit clearer):

   sudo parted -l

Create an new /dev/sdb1 partition (here I use with fdisk because parted could not create EXT4 file systems):

  sudo fdisk /dev/sdb
     c (disable msdos mode)
     u (set units to sectors)
     d (delete partition 1)
     1
     n (create new primary partition 1)
     p
     1
     <Enter>Use default first and last sectors
     <Enter>
     w (Write out the new partition table)

Check the /dev/sdb1 partition exists (but the file system column is blank):

   sudo parted -l

Now we make the EXT4 files system:

   sudo mkfs -t EXT4 /dev/sdb1

Now check the partition is now EXT4:

   sudo parted -l

Install BackupPC

Now we actuall install BackupPC:

   sudo apt-get install backuppc

Set the password for account 'backuppc':

   sudo htpasswd /etc/backuppc/htpasswd backuppc

Point your web browser at http:/backuppc and log in as 'backuppc' with the password you have just set up. The BackupPC Server Status page should be displayed (it doesn't matter if there are some failed backups listed at the bottom of the page).

Copy the Data Directory Contents

Copy the BackupPC data directory contents to the external hard disk drive:

   sudo cp -r /var/lib/backuppc /media/usb0

And set its owner to 'backuppc':

   sudo chown -R backuppc:backuppc /media/usb0/backuppc

Check the new data directory is present and has the right permissions:

   sudo ls -al /media/usb0

And check its contents:

   sudo ls -al /media/usb0/backuppc

Set up a Symbolic Link from the Old Location to the New

Remove the old BackupPC data directory:

   sudo rm -r /var/lib/backuppc

And replace it with a symbolic link to the new data directory (note the order of the parameters is target path before link path):

   sudo ln -s /media/usb0/backuppc /var/lib/backuppc

Set the owner of the symbolic link to 'backuppc':

   sudo chown -h backuppc:backuppc /var/lib/backuppc

Check the symbolic link is present and has the right permissions:

   sudo ls -al /var/lib

And check that it links to the right contents:

   sudo ls -al /var/lib/backuppc

Restart the server (just to make sure everything reinitializes):

   sudo shutdown -r now

Point your web browser at http:/backuppc. The BackupPC Server Status page should be displayed. BackupPC is running with the data directory on the external hard disk drive.

How to disable the Guest Account in Ubuntu 10.04 LTS

I just noticed an option to log in as 'guest' on our Ubuntu laptop.  I cannot remember asking for it, and I certainly don't want it, so I looked for a way to disable it.  In Ubuntu 10.04 LTS the guest option is provided by the package gdm-guest-session.  I went into the Synaptic package manager and uninstalled it.  After logging out and in again, the guest option is no more.

A 404 Not Found Error on Installing BackupPC on Ubuntu 10.04 LTS

I recently installed BackupPC on my Ubuntu 10.04 LTS web server. I did this by entering 'sudo apt-get install backuppc'. Initially I couldn't get the backuppc web interface to work. Going to http://192.168.0.1/backuppc in a web browser only gave a '404 Not Found' error.

I tracked down the reason for this to me having failed to explicitly selected 'Apache2' as the BackupPC web server. During installation a page something like this had been presented:

      Select web server

[ ] Apache2

       <ok>    

I had just hit <enter> assuming that 'Apache2' was the default (there were no other alternatives after all). What I should have done was hit the spacebar to select 'Apache2' and then hit <enter>.

I fixed the problem by completely removing BackupPC ('sudo apt-get purge backuppc') and then reinstalling ('sudo apt-get install backuppc') taking care to hit the spacebar at the appropriate point.

The lack of clear instructions on the above installation page might be regarded as a bug in the BackupPC installation process.

Update on Mon 2012-02-27 by Tristram Brelstaff

It turns out that I had an almost identical problem a year and half ago when installing PhpMyAdmin.