BBL solved with Clingo ASP in 0.031 seconds

This just reproduces the example in the text, but anyway.

Consider the KIF of BBL, with comment lines ';' removed.  The following Python code turns this into a Clingo ASP (parser part from Peter Norvig):

from __future__ import division
import sys

Symbol = str # A Lisp Symbol is implemented as a Python str
List = list # A Lisp List is implemented as a Python list
Number = (int, float) # A Lisp Number is implemented as a Python int or float

################ Parsing: parse, tokenize, and read_from_tokens

def parse(program):
"Read a Scheme expression from a string."
return read_from_tokens(tokenize(program))

def tokenize(s):
"Convert a string into a list of tokens."
return s.replace('(',' ( ').replace(')',' ) ').split()

def atom(token):
"Numbers become numbers; every other token is a symbol."
try: return int(token)
except ValueError:
try: return float(token)
except ValueError:
return Symbol(token)

def read_from_tokens(tokens):
"Read an expression from a sequence of tokens."
if len(tokens) == 0:
raise SyntaxError('unexpected EOF while reading')
token = tokens.pop(0)
if '(' == token:
L = []
while tokens[0] != ')':
L.append(read_from_tokens(tokens))
tokens.pop(0) # pop off ')'
return L
elif ')' == token:
raise SyntaxError('unexpected )')
else:
return atom(token)

def rewrite_init(s):
[init,F]=s
return ['true',F,1]

def rewrite_next(s):
[nxt,F]=s
return ['true',F,['plus','T',1]]

def rewrite_does(s):
return ['does']+s[1:]+['T']

def rewrite_not(s):
return ['not', rewriter(s[1])]

def rewrite_rule(s):
return ['<=']+[rewriter(s[1])]+[['time', 'T']]+[rewriter(t) for t in s[2:]]

def rewrite_timed_atom(s):
return s+['T']

def rewriter(s):
if type(s)==type('a'):
return [s, 'T']
head = s[0]
if head in ['index', 'successor']:
return s
if head == 'init':
return rewrite_init(s)
elif head == 'next':
return rewrite_next(s)
elif head == 'not':
return rewrite_not(s)
elif head == 'does':
return rewrite_does(s)
elif head in ['role', 'base']:
return s
elif head == '<=':
return rewrite_rule(s)
else:
return rewrite_timed_atom(s)

def rewrite(gdl):
return [rewriter(rule) for rule in gdl]

def aspy(s):
if type(s) == type([]):
try:
if s[0] == '<=':
return aspy(s[1])+' :- '+', '.join([aspy(x) for x in s[2:]])
elif s[0] == 'plus':
return aspy(s[1])+'+'+aspy(s[2])
elif s[0] == 'not':
return 'not '+aspy(s[1])
else:
return s[0]+'('+','.join([aspy(x) for x in s[1:]])+')'
except:
return s[0]
elif type(s)==type('a') and s[0] == '?':
return s[1:].upper()
else:
return str(s)


if __name__ == '__main__':
with open('bbl.kif', 'r') as myfile:
program='('+myfile.read().replace('\n', '')+')'
gdl = parse(program)
gdlplus = rewrite(gdl)
with open('bbl.lp', 'w') as f:
for x,y in zip(gdl,gdlplus):
f.write(aspy(y)+'.\n')
f.write('1{ does(R,M,T) : input(R,M,T) }1 :- role(R), time(T).\n')
f.write(':- does(R,M,T), not legal(R,M,T).\n')
f.write(':- 0{ terminal(T) : time(T) }0.\n')
f.write(':- terminal(T), role(R), not goal(R,100,T).\n')
f.write('time(1..7).\n')

This produces the following .lp file:

role(robot).
base(p(X)) :- time(T), index(X).
base(q(X)) :- time(T), index(X).
base(r(X)) :- time(T), index(X).
base(step(1)).
base(step(2)).
base(step(3)).
base(step(4)).
base(step(5)).
base(step(6)).
base(step(7)).
input(robot,a(X),T) :- time(T), index(X).
input(robot,b(X),T) :- time(T), index(X).
input(robot,c(X),T) :- time(T), index(X).
index(1).
index(2).
index(3).
index(4).
index(5).
index(6).
index(7).
index(8).
index(9).
true(step(1),1).
legal(robot,a(X),T) :- time(T), index(X).
legal(robot,b(X),T) :- time(T), index(X).
legal(robot,c(X),T) :- time(T), index(X).
true(p(X),T+1) :- time(T), does(robot,a(X),T), not true(p(X),T).
true(p(X),T+1) :- time(T), does(robot,b(X),T), true(q(X),T).
true(p(X),T+1) :- time(T), true(p(X),T), not does(robot,a(X),T), not does(robot,b(X),T).
true(q(X),T+1) :- time(T), does(robot,b(X),T), true(p(X),T).
true(q(X),T+1) :- time(T), does(robot,c(X),T), true(r(X),T).
true(q(X),T+1) :- time(T), true(q(X),T), not does(robot,b(X),T), not does(robot,c(X),T).
true(r(X),T+1) :- time(T), does(robot,c(X),T), true(q(X),T).
true(r(X),T+1) :- time(T), true(r(X),T), not does(robot,c(X),T).
true(step(Y),T+1) :- time(T), true(step(X),T), successor(X,Y).
goal(robot,100,T) :- time(T), row(X,T).
goal(robot,0,T) :- time(T), not row(1,T), not row(2,T), not row(3,T), not row(4,T), not row(5,T), not row(6,T), not row(7,T), not row(8,T), not row(9,T).
terminal(T) :- time(T), row(X,T).
terminal(T) :- time(T), true(step(7),T).
row(X,T) :- time(T), true(p(X),T), true(q(X),T), true(r(X),T).
successor(1,2).
successor(2,3).
successor(3,4).
successor(4,5).
successor(5,6).
successor(6,7).
1{ does(R,M,T) : input(R,M,T) }1 :- role(R), time(T).
:- does(R,M,T), not legal(R,M,T).
:- 0{ terminal(T) : time(T) }0.
:- terminal(T), role(R), not goal(R,100,T).
time(1..7).

Running this through Clingo then gives the solution

clingo version 4.5.1
Reading from bbl.lp
Solving...
Answer: 1
role(robot) base(step(1)) base(step(2)) base(step(3)) base(step(4)) base(step(5)) base(step(6)) base(step(7)) index(1) index(2) index(3) index(4) index(5) index(6) index(7) index(8) index(9) true(step(1),1) successor(1,2) successor(2,3) successor(3,4) successor(4,5) successor(5,6) successor(6,7) time(1) time(2) time(3) time(4) time(5) time(6) time(7) base(p(1)) base(p(2)) base(p(3)) base(p(4)) base(p(5)) base(p(6)) base(p(7)) base(p(8)) base(p(9)) base(q(1)) base(q(2)) base(q(3)) base(q(4)) base(q(5)) base(q(6)) base(q(7)) base(q(8)) base(q(9)) base(r(1)) base(r(2)) base(r(3)) base(r(4)) base(r(5)) base(r(6)) base(r(7)) base(r(8)) base(r(9)) input(robot,a(1),1) input(robot,a(2),1) input(robot,a(3),1) input(robot,a(4),1) input(robot,a(5),1) input(robot,a(6),1) input(robot,a(7),1) input(robot,a(8),1) input(robot,a(9),1) input(robot,a(1),2) input(robot,a(2),2) input(robot,a(3),2) input(robot,a(4),2) input(robot,a(5),2) input(robot,a(6),2) input(robot,a(7),2) input(robot,a(8),2) input(robot,a(9),2) input(robot,a(1),3) input(robot,a(2),3) input(robot,a(3),3) input(robot,a(4),3) input(robot,a(5),3) input(robot,a(6),3) input(robot,a(7),3) input(robot,a(8),3) input(robot,a(9),3) input(robot,a(1),4) input(robot,a(2),4) input(robot,a(3),4) input(robot,a(4),4) input(robot,a(5),4) input(robot,a(6),4) input(robot,a(7),4) input(robot,a(8),4) input(robot,a(9),4) input(robot,a(1),5) input(robot,a(2),5) input(robot,a(3),5) input(robot,a(4),5) input(robot,a(5),5) input(robot,a(6),5) input(robot,a(7),5) input(robot,a(8),5) input(robot,a(9),5) input(robot,a(1),6) input(robot,a(2),6) input(robot,a(3),6) input(robot,a(4),6) input(robot,a(5),6) input(robot,a(6),6) input(robot,a(7),6) input(robot,a(8),6) input(robot,a(9),6) input(robot,a(1),7) input(robot,a(2),7) input(robot,a(3),7) input(robot,a(4),7) input(robot,a(5),7) input(robot,a(6),7) input(robot,a(7),7) input(robot,a(8),7) input(robot,a(9),7) input(robot,b(1),1) input(robot,b(2),1) input(robot,b(3),1) input(robot,b(4),1) input(robot,b(5),1) input(robot,b(6),1) input(robot,b(7),1) input(robot,b(8),1) input(robot,b(9),1) input(robot,b(1),2) input(robot,b(2),2) input(robot,b(3),2) input(robot,b(4),2) input(robot,b(5),2) input(robot,b(6),2) input(robot,b(7),2) input(robot,b(8),2) input(robot,b(9),2) input(robot,b(1),3) input(robot,b(2),3) input(robot,b(3),3) input(robot,b(4),3) input(robot,b(5),3) input(robot,b(6),3) input(robot,b(7),3) input(robot,b(8),3) input(robot,b(9),3) input(robot,b(1),4) input(robot,b(2),4) input(robot,b(3),4) input(robot,b(4),4) input(robot,b(5),4) input(robot,b(6),4) input(robot,b(7),4) input(robot,b(8),4) input(robot,b(9),4) input(robot,b(1),5) input(robot,b(2),5) input(robot,b(3),5) input(robot,b(4),5) input(robot,b(5),5) input(robot,b(6),5) input(robot,b(7),5) input(robot,b(8),5) input(robot,b(9),5) input(robot,b(1),6) input(robot,b(2),6) input(robot,b(3),6) input(robot,b(4),6) input(robot,b(5),6) input(robot,b(6),6) input(robot,b(7),6) input(robot,b(8),6) input(robot,b(9),6) input(robot,b(1),7) input(robot,b(2),7) input(robot,b(3),7) input(robot,b(4),7) input(robot,b(5),7) input(robot,b(6),7) input(robot,b(7),7) input(robot,b(8),7) input(robot,b(9),7) input(robot,c(1),1) input(robot,c(2),1) input(robot,c(3),1) input(robot,c(4),1) input(robot,c(5),1) input(robot,c(6),1) input(robot,c(7),1) input(robot,c(8),1) input(robot,c(9),1) input(robot,c(1),2) input(robot,c(2),2) input(robot,c(3),2) input(robot,c(4),2) input(robot,c(5),2) input(robot,c(6),2) input(robot,c(7),2) input(robot,c(8),2) input(robot,c(9),2) input(robot,c(1),3) input(robot,c(2),3) input(robot,c(3),3) input(robot,c(4),3) input(robot,c(5),3) input(robot,c(6),3) input(robot,c(7),3) input(robot,c(8),3) input(robot,c(9),3) input(robot,c(1),4) input(robot,c(2),4) input(robot,c(3),4) input(robot,c(4),4) input(robot,c(5),4) input(robot,c(6),4) input(robot,c(7),4) input(robot,c(8),4) input(robot,c(9),4) input(robot,c(1),5) input(robot,c(2),5) input(robot,c(3),5) input(robot,c(4),5) input(robot,c(5),5) input(robot,c(6),5) input(robot,c(7),5) input(robot,c(8),5) input(robot,c(9),5) input(robot,c(1),6) input(robot,c(2),6) input(robot,c(3),6) input(robot,c(4),6) input(robot,c(5),6) input(robot,c(6),6) input(robot,c(7),6) input(robot,c(8),6) input(robot,c(9),6) input(robot,c(1),7) input(robot,c(2),7) input(robot,c(3),7) input(robot,c(4),7) input(robot,c(5),7) input(robot,c(6),7) input(robot,c(7),7) input(robot,c(8),7) input(robot,c(9),7) legal(robot,a(1),1) legal(robot,a(2),1) legal(robot,a(3),1) legal(robot,a(4),1) legal(robot,a(5),1) legal(robot,a(6),1) legal(robot,a(7),1) legal(robot,a(8),1) legal(robot,a(9),1) legal(robot,a(1),2) legal(robot,a(2),2) legal(robot,a(3),2) legal(robot,a(4),2) legal(robot,a(5),2) legal(robot,a(6),2) legal(robot,a(7),2) legal(robot,a(8),2) legal(robot,a(9),2) legal(robot,a(1),3) legal(robot,a(2),3) legal(robot,a(3),3) legal(robot,a(4),3) legal(robot,a(5),3) legal(robot,a(6),3) legal(robot,a(7),3) legal(robot,a(8),3) legal(robot,a(9),3) legal(robot,a(1),4) legal(robot,a(2),4) legal(robot,a(3),4) legal(robot,a(4),4) legal(robot,a(5),4) legal(robot,a(6),4) legal(robot,a(7),4) legal(robot,a(8),4) legal(robot,a(9),4) legal(robot,a(1),5) legal(robot,a(2),5) legal(robot,a(3),5) legal(robot,a(4),5) legal(robot,a(5),5) legal(robot,a(6),5) legal(robot,a(7),5) legal(robot,a(8),5) legal(robot,a(9),5) legal(robot,a(1),6) legal(robot,a(2),6) legal(robot,a(3),6) legal(robot,a(4),6) legal(robot,a(5),6) legal(robot,a(6),6) legal(robot,a(7),6) legal(robot,a(8),6) legal(robot,a(9),6) legal(robot,a(1),7) legal(robot,a(2),7) legal(robot,a(3),7) legal(robot,a(4),7) legal(robot,a(5),7) legal(robot,a(6),7) legal(robot,a(7),7) legal(robot,a(8),7) legal(robot,a(9),7) legal(robot,b(1),1) legal(robot,b(2),1) legal(robot,b(3),1) legal(robot,b(4),1) legal(robot,b(5),1) legal(robot,b(6),1) legal(robot,b(7),1) legal(robot,b(8),1) legal(robot,b(9),1) legal(robot,b(1),2) legal(robot,b(2),2) legal(robot,b(3),2) legal(robot,b(4),2) legal(robot,b(5),2) legal(robot,b(6),2) legal(robot,b(7),2) legal(robot,b(8),2) legal(robot,b(9),2) legal(robot,b(1),3) legal(robot,b(2),3) legal(robot,b(3),3) legal(robot,b(4),3) legal(robot,b(5),3) legal(robot,b(6),3) legal(robot,b(7),3) legal(robot,b(8),3) legal(robot,b(9),3) legal(robot,b(1),4) legal(robot,b(2),4) legal(robot,b(3),4) legal(robot,b(4),4) legal(robot,b(5),4) legal(robot,b(6),4) legal(robot,b(7),4) legal(robot,b(8),4) legal(robot,b(9),4) legal(robot,b(1),5) legal(robot,b(2),5) legal(robot,b(3),5) legal(robot,b(4),5) legal(robot,b(5),5) legal(robot,b(6),5) legal(robot,b(7),5) legal(robot,b(8),5) legal(robot,b(9),5) legal(robot,b(1),6) legal(robot,b(2),6) legal(robot,b(3),6) legal(robot,b(4),6) legal(robot,b(5),6) legal(robot,b(6),6) legal(robot,b(7),6) legal(robot,b(8),6) legal(robot,b(9),6) legal(robot,b(1),7) legal(robot,b(2),7) legal(robot,b(3),7) legal(robot,b(4),7) legal(robot,b(5),7) legal(robot,b(6),7) legal(robot,b(7),7) legal(robot,b(8),7) legal(robot,b(9),7) legal(robot,c(1),1) legal(robot,c(2),1) legal(robot,c(3),1) legal(robot,c(4),1) legal(robot,c(5),1) legal(robot,c(6),1) legal(robot,c(7),1) legal(robot,c(8),1) legal(robot,c(9),1) legal(robot,c(1),2) legal(robot,c(2),2) legal(robot,c(3),2) legal(robot,c(4),2) legal(robot,c(5),2) legal(robot,c(6),2) legal(robot,c(7),2) legal(robot,c(8),2) legal(robot,c(9),2) legal(robot,c(1),3) legal(robot,c(2),3) legal(robot,c(3),3) legal(robot,c(4),3) legal(robot,c(5),3) legal(robot,c(6),3) legal(robot,c(7),3) legal(robot,c(8),3) legal(robot,c(9),3) legal(robot,c(1),4) legal(robot,c(2),4) legal(robot,c(3),4) legal(robot,c(4),4) legal(robot,c(5),4) legal(robot,c(6),4) legal(robot,c(7),4) legal(robot,c(8),4) legal(robot,c(9),4) legal(robot,c(1),5) legal(robot,c(2),5) legal(robot,c(3),5) legal(robot,c(4),5) legal(robot,c(5),5) legal(robot,c(6),5) legal(robot,c(7),5) legal(robot,c(8),5) legal(robot,c(9),5) legal(robot,c(1),6) legal(robot,c(2),6) legal(robot,c(3),6) legal(robot,c(4),6) legal(robot,c(5),6) legal(robot,c(6),6) legal(robot,c(7),6) legal(robot,c(8),6) legal(robot,c(9),6) legal(robot,c(1),7) legal(robot,c(2),7) legal(robot,c(3),7) legal(robot,c(4),7) legal(robot,c(5),7) legal(robot,c(6),7) legal(robot,c(7),7) legal(robot,c(8),7) legal(robot,c(9),7) true(p(9),2) does(robot,a(9),1) true(p(9),5) does(robot,a(9),4) true(p(9),7) does(robot,a(9),6) does(robot,a(9),7) does(robot,b(9),2) does(robot,b(9),5) true(q(9),3) true(q(9),6) true(q(9),7) true(q(9),8) does(robot,c(9),3) true(r(9),4) true(r(9),5) true(r(9),6) true(r(9),7) true(r(9),8) true(step(2),2) true(step(3),3) true(step(4),4) true(step(5),5) true(step(6),6) true(step(7),7) row(9,7) goal(robot,100,7) goal(robot,0,1) goal(robot,0,2) goal(robot,0,3) goal(robot,0,4) goal(robot,0,5) goal(robot,0,6) terminal(7)
SATISFIABLE

Models : 1+
Calls : 1
Time : 0.218s (Solving: 0.20s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.031s

I think this approach will sort out at least a few of the Competition single-player games.  Sudoko is another story, although maybe not: Clingo is designed to go after NP-complete SAT problems.