Results of a series of experiments on the crossover point in random 3SAT. Also details of the TABLEAU algorithm.
Experimental results on the behavior of implicates in randomly-generated problems. This work has ramifications for knowledge-compilation as well as satisfiability checking.
Largely superseded by the journal paper above.
An obscure paper containing a good idea. Local search is used to identify the important variables on which the systematic search then branches. This should work well on structured problems -- unfortunately, in this paper I did all my experiments on randomly generated problems...
An overview of an interesting spring symposium.
Gives a general method for utilizing symmetries in propositional satisfiability problems. Utilizes techniques from computational group theory.
An older (and not as good) paper on a similar topic. Interesting primarily for the proof that symmetry detection is equivalent to graph isomorphism.
A description of the CIRL scheduler and its use on benchmark problems relevant to aircraft manufacture. Gives details of the doubleback optimization algorithm.
Compares various SAT algorithms on scheduling problems and concludes that randomly generated problems are not necessarily a good predictor of success on structured problems.
Outlines an approach to making default reasoning tractable by approximating the consistency check.
Reasoning about action is hard.
Shows how to handle a class of problems in reasoning about action by importing ideas for qualitative reasoning. I believe that this is the first paper to suggest that observations need to be treated specially in reasoning about action.
Shows how path-based rules (i.e., ALL-style rules -- see below) can be cleanly combined with object-oriented programming.
Stakes out a middle ground between expert systems and qualitative modeling, and argues that in some domains this is the right level of abstraction for diagnosis.
Draws parallels between work in AI on tractable reasoning and studies of human common-sense reasoning.
Outlines an approach to knowledge-representation and reasoning in which direct "inferential" reasoning is done immediately (tractably) but reasoning by cases (or, equivalently, proof by contradiction) requires user guidance.
An overview of Algernon -- the implementation of Access-Limited Logic (ALL).
An early ALL/Algernon paper.
The definitive reference on ALL and Algernon.
The first ALL paper. Defines the notion of "Socratic Completeness".
Explains when and why qualitative simulation is better than Monte Carlo methods.
QPC is am implemented system that "compiles" QPE-style processes and views into a QSIM-style QDE. One of the precursors to CME.