James M. Crawford

An annotated list of papers is available.

He co-chaired the satisfiability competition at the "International Competition and Sympoisium on Satisfiability Testing" held in Beijing China. The guidelines for the competition are available, as are the benchmark problems.

Research

Knowledge representation

As part of my dissertation I developed a knowledge-representation system called "Algernon". Algernon combines frame-based knowledge-representation with inference rules and aims to provide efficient inference while maintaining a clear semantics. Algernon has been used to support Elaine Rich's natural language project at MCC, to teach the expert system's class at the University of Texas, and to support the building of a prototype system combining rule-based and model-based reasoning at AT&T. Ongoing work is focusing on re-implementing the rule engine (we are particularly interested in investigating rule compilation), and on understanding the relationship between the inferential limitations built into Algernon (for computational reasons) and inferential limitations in human reasoning.

Satisfiability

Determining whether a propositional theory is satisfiable is a prototypical example of an NP-complete problem. Furthermore, many problems that occur in knowledge representation, learning, planning, and other areas of AI are essentially satisfiability problems. Much interesting experimental work has recently been done in AI on randomly-generated satisfiability problems. It appears that as problems become more constrained (i.e., the clause/variable ratio is increased) there is a "cross-over point" at which the probability of a randomly-chosen theory being satisfiable drops quite quickly from almost one to almost zero. Further, the problems around this cross-over point seem to be quite hard. We have found empirically that, for 3-SAT, the number of clauses at the crossover point is a linear function of the number of variables. There is much additional work to be done here , e.g., trying out new ideas for speeding up satisfiability checking, translating from LISP to very fast C code, applying these ideas and results to more practical problems, etc.

The code for tableau is available for research purposes as a tar archive. This includes both the SAT checker tableau (more or less as described in Experimental Results on the Crossover Point in Random 3SAT. but without the data-structures tuned for random 3SAT) and a polynomial-time preprocessor ("compact") that may be useful in other systems. Warning: This is research code. Comments are minimal and much of it was written before I even heard of ANSI standard C.

Contact Information