Abstract

I have been involved in the design and implementation of reasoners for (almost) fifteen years. During this time I have had the mixed fortune to have implemented three systems for two very different sorts of logics in three programming languages (plus an attempt using a fourth language). In this talk I will describe some of this work and expound on the lessons I (painfully) learned. Some of these lessons were quite a surprise to me; others run counter to the perceived management wisdom of the time.

This work has been carried out with a number of colleagues, most notably

• Ian Horrocks
• Roberto Sebastiani

This talk was given as an invited talk at the IJCAR-2001 Workshop on Issues in the Design and Experimental Evaluation of Systems for Modal and Temporal Logics. Sienna, Italy, June 2001.

History

Logics:

inexpressive, expressive

Systems:

CLASSIC, NeoClassic,, DLP

Languages:

Lisp, C++, Java, ML

Years:

• 1986-1988 - Kandor (maintenance)
• 1989-1994 - CLASSIC
• 1994-1997 - NeoClassic
• 1998-2001 - DLP

CLASSIC

• reasoner for inexpressive Description Logic
  • no disjunction
  • reasoning algorithm not known
  • nearly polynomial reasoning
• implemented in LISP
• designed for fast question answering
  • builds data structures to hold completed form of input

The Language of CLASSIC

<concept-expression>	::= THING | CLASSIC-THING
	| HOST-THING | <concept-name>
	| (AND <concept-expression>+)
	| (ALL <role-name> <concept-expression>)
	| (ATLEAST <positive-integer> <role-name>)
	| (ATMOST <positive-integer> <role-name>)
	| (FILLS <role-name> <individual-name>+
	| (SAMEAS <attribute-path> <attribute-path>)
	| (TESTC <function> <arg>*
	| (TESTH <function> <arg>*
	| (ONEOF <individual-name>)
	| (MAX <number>)
	| (MIN <number>)
<individual-expression>	::= <concept-expression>
<rule>	::= (<concept-name> <concept-expression>)

NeoClassic

• reimplementation of Classic
  • minor changes in language
• written in C++
• designed similarly to Classic
  • better low-level data structures

Experiences from CLASSIC and NeoClassic

• building reasoners for inexpressive languages can be difficult
  • lots of constructs in language
  • complex data structures
  • getting the reasoning right
• picking the right language can made a big difference
  • building NeoClassic was much harder than building CLASSIC
• limited languages can be effective for some tasks

DLP

• reasoner for expressive Description Logic (or Modal Logic)
  • disjunction, negation, transitive roles
  • basic reasoning algorithms well known
  • reasoning exponential time complete
• implemented in ML (Standard ML of New Jersey)
• designed for fast reasoning
  • uses an optimized tableau method
  • incorporates other optimizations
• has one known bug involving transitive closure of roles

The (A) Language of DLP

Concepts	<concept name>
	TOP
	BOTTOM
	NUMBER
	STRING
	(NOT <concept>)
	(AND <concept>+)
	(OR <concept>+)
	(SOME <role> <concept>)
	(ALL <role> <concept>)
	(ATLEAST <n> <concept>)
	(ATMOST <n> <concept>)
Roles	<role name>

Roles can be defined to be transitive.

Main Optimizations in DLP

Normalisation

• transform into a normalised form
• perform simplifications

BCP

look for places with only one choice and perform them first

Semantic Branching

pick a ``variable'' and assign it to true or false, instead of picking a disjunction and assigning a disjunct to true

Backjumping

when backtracking skip over choices that did not contribute to the failure

Caching

remember and reuse results of modal sub-problems

Heuristics

heuristics to enhance backjumping or BCP

Effects of Optimizations

Total Tableaux'98 problems solved

Optimisation Removed	Oldest-random	Oldest-JW	JW	Random
NONE	967	915	936	874
Caching	882	826	851	671
Backjumping	880	847	877	795
Semantic Branching	849	---	---	851
BCP	932	873	879	839
Normalisation	911	913	931	781

Effects of Optimizations

Provable S4 Tableaux'98 problems solved

Optimisation Removed	Heuristic	45	branch	grz	ipc	md	path	ph	s5	t4p
NONE	Oldest-random	21	18	21	10	3	15	7	21	21
	Oldest-JW	21	21	21	10	3	8	5	21	21
	JW	21	18	21	10	3	9	5	21	21
	Random	21	18	21	21	4	7	7	21	21
Caching	Oldest-random	21	18	21	8	7	8	7	21	21
	Oldest-JW	21	21	21	7	7	5	5	10	21
	JW	21	18	21	7	7	6	5	21	21
	Random	21	18	0	13	4	3	7	21	21
Backjumping	Oldest-random	21	17	21	9	3	3	7	2	21
	Oldest-JW	21	21	21	9	3	3	4	2	18
	JW	21	17	21	9	3	3	4	4	21
	Random	21	17	21	8	3	3	5	4	21
Semantic Branching	Oldest-random	15	18	21	7	3	3	7	4	7
	Random	15	18	21	7	3	3	7	4	7
BCP	Oldest-random	21	15	21	10	3	11	6	21	21
	Oldest-JW	21	21	21	10	3	7	4	15	21
	JW	21	12	21	10	3	8	4	21	21
	Random	21	16	21	21	4	7	6	21	21
Normalisation	Oldest-random	21	18	7	10	3	9	6	21	21
	Oldest-JW	21	21	21	10	3	10	6	21	21
	JW	21	16	21	10	3	9	6	21	21
	Random	21	10	21	21	4	7	7	4	21

Effects of Optimizations

Classification times for Galen knowledge base (CPU seconds)

Optimisation Removed	Oldest-random	Oldest-JW	JW	Random
NONE	70	172	153	37
Caching	399	1182	1005	326
Backjumping	>10,000	>10,000	>10,000	>10,000
Semantic Branching	2087	---	---	319
BCP	90	431	616	40
Normalisation	87	207	162	39

Effects of Optimizations

Comparisons with older systems:
Median Solution times for PS12 Formulae
Median Solution times for PS13 Formulae

Comparisons between optimizations:
Solution times for K-dum-n
Solution times for S4-s5-p
Median solution times for PS12 formulae
90th percentile solution times for PS12 formulae

Experiences from DLP

• building reasoners for expressive languages can be simple
  • few constructs in language
  • data structures don't have to be too complex
  • theoretical work very helpful
• picking the right language can made a huge difference
  • first core of DLP built in less than one month
• correct optimizations are vital for decent performance
  • normalization, backjumping, caching

Lessons

• most important
  • reasoning optimizations
  • programming language
  • good characterization of reasoning in the logic
  • flexibility of system
• more important
  • data structure optimizations (n to log n)
  • small, concentrated development team for core of reasoner
  • heuristics
• least important
  • constant factor optimizations (but can be important in some areas)

Surprises

• expressive reasoners can be as fast as inexpressive reasoners
  • DLP is as fast as CLASSIC (for many things) on CLASSIC KBs
• some optimizations are incredibly effective
  • normalization, divide and conquer, caching, backjumping
• some optimizations are ineffective
  • some heuristics

Facts

• computational complexity issues
  • worst-case complexity is (nearly) useless to determine what to do
  • normal-case or average-case complexity is not useful either
• reasoning optimizations restrict the class of logics
  • invalid for some logics

Management Wisdom

Use accepted practices

• standard libraries (standard components, e.g., sets)
  • can be incredibly wrong for our purposes
    • assume large sets, but we mostly have empty sets
  • build your own libraries for the parts that count
• standard languages (C, C++, Java)
  • can be incredibly inefficient
    • require garbage collection support
    • require templates for many things
      • end up with very large object files
    • are extremely verbose
  • use the language that fits and works best

Most Important Lesson

Building a new reasoner is an exploration

• don't make your reasoner too rigid by too-early (data structure) optimizations
• design and implement your system so that it can incorporate different reasoning optimizations
• design and implement your system so that it is easy to debug
• perform empirical analysis to see which optimizations are effective (and which are not)