Queens on a chessboard with Caduceus

From Openproofs

Caduceus has been used to solve a simple "N-queens on a chessboard" problem. More information about the Queens problem with Caduceus is available on-line; the slides are a good place to start and there is a paper with more detail.

It's a tiny toy problem, but useful for teaching how to develop proofs. Jean-Christophe Filliâtre notes that "in two lines of code we have C idiomatic bitwise operations, loops & recursion involved in a backtracking algorithm, and highly efficient code".

This is an open proof because:

• The implementation is FLOSS, more specifically, the software being proved is in the public domain. See below.
• The proof is FLOSS. The proof is included in the Caduceus distribution, all of which was released under the GNU Public License (GPL) version 2.
• Required tools are FLOSS. It can be modified with FLOSS text editors, the code can be compiled with a FLOSS C compiler (such as gcc), and the Caduceus tool (used for proof) is released under the GPL. The tools necessary to support Caduceus (e.g., Why, alt-ergo, and Coq or PVS) are FLOSS as well.

This program was originally written in 2 obscure lines; it can be reformatted (and a minor ANSI C error fixed) into this more readable program: <source lang="c">

int t(int a, int b, int c) {
 int d, e=a&;~b&;~c, f=1;
 if (a)
  for (f=0; d=e&;-e; e-=d)
   f += t(a-d,(b+d)*2,(c+d)/2));
 return f;
}
int main(int n) {
 return t(~(~0<<n),0,0);
}

</source>

This is a standalone C program which reads an integer n on standard input and prints the number of ways that n queens can be put on a n × n chessboard so that they do not attack each other. It requires that n be smaller than the machine word size in bits (typically 32).

Unfortunately, the original release did not determine the license that covered the software being evaluated. It is so short that it could be argued that copyright did not apply, but this is a shaky ground to stand on. David A. Wheeler tracked down the original author, who graciously released this code to the public domain. Here is his message (with some material modified to counter spam), showing that the original proved program is indeed FLOSS:

From marcel k, (at) bitpit.net Mon Feb 25 10:36:15 2008
Return-path: marcelk, (at) bitpit.net
Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed
Message-Id: F185DFA6-8AF8-4612-8F1F-DE55AB749FC9, at, bitpit.net
Content-Transfer-Encoding: 7bit
From: Marcel van Kervinck marcelk, (at) bitpit.net
Subject: Re: Would you release "queens" as Free Software / Open Source Software? (xyzzy)
Date: Mon, 25 Feb 2008 17:36:00 +0800
To: dwheeler, (at) dwheeler.com

Hello David,

I have no problem at all with your request.

I posted the queens program over 13 years ago on usenet with no
other thoughts than to share it openly without constraints (except
maybe attribution).

I think it is open by default in most countries by my posting
and by it being so small, but in case there is any doubt, I
hereby declare the program public domain explicitely:

Version 1

t(a,b,c){int d=0,e=a&~b&~c,f=1;if(a)for(f=0;d=(e-=d)&-e;f+=t(a-d,(b+d)*2,(
c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0<<q),0,0));}

This version unfortunately contains a bug that allows the compiler
to give it a different interpretation than intended. I should have
known better at the time when I posted it. Although it is wrong,
it is the original form in which it was posted and it may have some
odd kind of historical value for that reason.

Today I prefer the following version of the queens program:

Version 2

t(a,b,c){int d=0,e=a&~b&~c,f=1;if(a)for(f=0;e-=d,d=e&-e;f+=t(a-d,(b+d)*2,(
c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0<<q),0,0));}

Recently I found a rather trivial shorter version that also removes some
unnecessary obfuscation. For completeness, here it is:

Version 3

t(a,b,c){int d=0,e=a&~b&~c,f=1;if(a)for(f=0;d=e&-e;f+=t(a-d,(b+d)*2,(c+d)/
2))e-=d;return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0<<q),0,0));}

It is one character shorter and somewhat clearer, but it has lost
some of its "charm" in the process...

These other versions, as well as this e-mail, are also public domain
of course.

Kind regards,

	Marcel van Kervinck

On 20 Feb, 2008, at 23:23, David A. Wheeler wrote:

> Hi  - I have a strange request.
>
> The following 2-liner has been attributed to you:
> t(a,b,c){int d=0,e=a&~b&~c,f=1;if(a)for(f=0;d=(e-=d)&-e;f+=t(a-d,(b 
> +d)*2,(
> c+d)/2));return f;}main(q){scanf("%d",&q);printf("%d\n",t(~(~0<<q), 
> 0,0));}
>
> If you're the author, would you please release this as open source  
> software?
> A simple declaration that "I release this under the GNU GPL version  
> 2 or greater",
> or some other license that you decide (such as LGPL, BSD-new, MIT),  
> would be enough.
> Or just declare that it's in the public domain, that'd be fine too.
>
> The reason is that I'm trying to encourage development of "open  
> proofs" -
> programs where EVERYTHING (programs, compilation tools, specs,  
> proofs, and
> proof tools) are Free-Libre / Open Source Software (FLOSS).  This  
> would help.
>
> Thanks.
>
> --- David A. Wheeler
>