Author name cluster

James M. Crawford

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

1 author row

AAAI Conference 1998 Conference Paper

A Non-Deterministic Semantics for Tractable Inference

James M. Crawford

Unit resolution is arguably the most useful known algorithm for tractable reasoning in propositional logic. Intuitively, if one knows a, b, and a ∧ b ⊃ c, then c should be an obvious implication. However, devising a tractable semantics that allows unit resolution has proven to be an elusive goal. We propose a 3-valued semantics for a tractable fragment of propositional logic that is inherently non-deterministic: the denotation of a formula is not uniquely determined by the denotation of the variables it contains. We show that this semantics yields a tractable, sound and complete, decision procedure. We generalize this semantics to a family of semantics, tied to Dalal’s notion of intricacy, of increasing deductive power and computational complexity.

PDF Details

AIJ Journal 1996 Journal Article

Experimental results on the crossover point in random 3-SAT

James M. Crawford
Larry D. Auton

Determining whether a propositional theory is satisfiable is a prototypical example of an NP-complete problem. Further, a large number of problems that occur in knowledge-representation, learning, planning, and other areas of AI are essentially satisfiability problems. This paper reports on the most extensive set of experiments to date on the location and nature of the crossover point in satisfiability problems. These experiments generally confirm previous results with two notable exceptions. First, we have found that neither of the functions previously proposed accurately models the location of the crossover point. Second, we have found no evidence of any hard problems in the under-constrained region. In fact the hardest problems found in the under-constrained region were many times easier than the easiest unsatisfiable problems found in the neighborhood of the crossover point. We offer explanations for these apparent contradictions of previous results.

Details DOI

AIJ Journal 1996 Journal Article

Implicates and prime implicates in Random 3-SAT

Robert Schrag
James M. Crawford

It has been observed previously that Random 3-SAT exhibits a phase transition at a critical ratio of constraints to variables, where the average frequency of satisfiability falls abruptly from near 1 to near 0. In this paper we look beyond satisfiability to implicates and prime implicates of non-zero length and show experimentally that, for any given length, these exhibit their own phase transitions. All of these phase transitions appear to share the same critical point as the well-known satisfiability phase transition. We also find a rich, regular pattern, in which phase transitions for longer implicates or prime implicates are less steep at a given problem size and all the phase transitions sharpen with increasing problem size. Implicates correspond in a one-to-one way to nogoods, and prime implicates correspond similarly to minimal nogoods. Knowledge about these phase transitions helps us to understand more about the behavior of search algorithms and knowledge compilation approaches in the context of Random 3-SAT.

Details DOI

AAAI Conference 1996 Conference Paper

Path-Based Rules in Object-Oriented Programming

James M. Crawford
Diane Litman

Object-oriented programming has recently emerged as one of the most important programming paradigms. While object-oriented programming clearly owes an intellectual debt to AI, it appears to be displacing some AI techniques, such as rule-based programming, from the marketplace. This need not be so as path-based rules-forward-chaining production rules that are restricted to follow pointers between objects-fit into the object-oriented paradigm in a clean and elegant way. The combination of path-based rules and object-oriented programming should be useful in AI applications, and in the more general problem of transferring AI techniques to the larger computer science community.

PDF Details

AAAI Conference 1994 Conference Paper

Experimental Results on the Application of Satisfiability Algorithms to Scheduling Problems

James M. Crawford

Considerable progress has been made in recent years in understanding and solving propositional satisfiabilit y problems. Much of this work has been based on experiments on randomly generated 3SAT problems. One generally accepted shortcoming of this work is that it is not clear how the results and algorithms developed will carry over to “real” constraintsatisfaction problems. This paper reports on a series of experiments applying satisfiability algorithms to scheduling problems. We have found that scheduling problems bear fairly little resemblance to the previously studied hard randomly generated 3SAT problems. In particular, scheduling problems tend to be quite large but under-constrained, Further, forward checking (e. g. , unit propagation) seems to be much more important on these problems than on hard random 3SAT problems. We have also found that the domain-specific heuristics developed to solve scheduling problems make surprisingly little difference in the time required to solve the problems. We suggest that the best algorithms for this problem class will probably be hill-climbing algorithms that incorporate some sort of forward checking.

PDF Details

AAAI Conference 1993 Conference Paper

Experimental Results on the Crossover Point in Satisfiability Problems

James M. Crawford

Determining whether a propositional theory is satisfiable is a prototypical example of an NPcomplete problem. Further, a large number of problems that occur in knowledge representation, learning, planning, and other areas of AI are essentially satisfiability problems. This paper reports on a series of experiments to determine the location of the crossu2rer point - the point at which half the randomly generated propositional theories with a given number of variables and given number of clauses are satisfiable - and to assess the relationship of the crossover point to the difficulty of determining satisfiability. We have found empirically that, for Q-SAT, the number of clauses at the crossover point is a linear function of the number of variables. This result is of theoretical interest since it is not clear why such a linear relationship should exist, but it is also of practical interest since recent experiments [Mitchell et al. 92; Cheeseman et al. 911 indicate that the most computationally difficult problems tend to be found near the crossover point. We have also found that for random 3-SAT problems below the crossover point, the average time complexity of satisfiability problems seems empirically to grow linearly with problem size. At and above the crossover point the complexity seems to grow exponentially, but the rate of growth seems to be greatest near the crossover point.

PDF Details

AAAI Conference 1992 Conference Paper

Formalizing Reasoning about Change: A Qualitative Reasoning Approach (Preliminary Report)

James M. Crawford

The development of a formal logic for reasoning about change has proven to be surprisingly difficult. Furthermore, the logics that have been developed have found surprisingly little application in those fields, such as Qualitative Reasoning, that are concerned with building programs that emulate human common-sense reasoning about change. In this paper, we argue that a basic tenet of qualitative reasoning practice-the separation of modeling and simulation-obviates many of the difficulties faced by previous attempts to formalize reasoning about change. Our analysis helps explain why the QR community has been nonplussed by some of the problems studied in the nonmonotonic reasoning community. Further, the formalism we present provides both the beginnings of a formal foundation for qualitative reasoning, and a framework in which to study a number of open problems in qualitative reasoning.

PDF Details