I analyzed the distribution that Goldberg used and found that it, rather than DPLL, was responsible for this amazing result: specifically, I showed that any random assignment is a solution to a randomly generated input with probability tending to 1 as the number of variables increases. I proposed an alternative distribution, now known as the constant-width distribution. The constant-width distribution comes with a parameter called density. I showed that the DPLL variant considered by Goldberg performs inefficiently on random inputs generated according to the constant-width distribution, regardless of density.

With collaborators, I further showed that random constant-width formulas nearly never have a true assignment if the density is greater than a constant times 2^k, where k is the disjunction size. I introduced non-backtracking variants of DPLL which are now known in the literature as UC, GUC, and UC with majority rule and showed that each of these performed efficiently on almost all random instances when density is less than a constant times 2^k/k - the constant depending on the variant.

We applied the techniques used to obtain the above results to estimate the impact of certain classes of SAT that are known to be solved efficiently without search. There are many such classes but some of the best known are 2-SAT, Horn, q-Horn, Extended Horn, Hidden Horn, CC-balanced, Linear Autarkies, and Matched formulas. The q-Horn class is especially interesting because, before our analysis, it had been thought to be the largest succinctly expressible, efficiently solved class of CNF formulas. We showed that some of these classes, including q-Horn, represent a substantial fraction of input formulas only if density is less than a constant times k and others only if density is less than a constant. None of the classes is substantially large up to densities on the order of even 2^k/k. We introduced another efficiently solved class called SLUR (for Single Lookahead Unit Resolution) and showed it subsumes most of the classes above. However, SLUR is no larger in the probabilistic sense than the trivial Matched class.

Our probabilistic studies have provided insights which have had some influence on SAT solver design and, more importantly, have helped to understand the boundaries of efficiently solved problems: the structures that allow such problems to be solved efficiently, and the structures that prevent formulas from being members of efficiently solved classes. The constant-width distribution remains to this day the most important distribution for analysis and interpreting SAT algorithmic behavior and has been used effectively by physicists to help understand what happens to solution structure as density increases.

Our more recent research attempts to transfer some of the knowledge gained from our previous research and some new problem solving ideas to the real world. Doing so required building our own testing tool which became the SBSAT solver mentioned earlier. SBSAT is unique in several ways and I mention the two most interesting ways here. First, SBSAT is non-clausal. All other modern SAT solvers depend on CNF inputs but few real problems are naturally expressed that way. Thus, problems must be translated to CNF from some other language, for example temporal logic, and the translation tends to garble critical domain-specific information that would otherwise be useful in directing a search for a solution. SBSAT bypasses the translation step. It is designed to memoize domain-specific information in preprocessing and use it to guide the search. SBSAT maintains a collection of state machines, the nodes and edges of which retain data such as how many inferences might be generated deeper in the search if a particular unassigned variable is assigned a particular value. Thus, SBSAT uses a new form of look-ahead, which we call function-complete look-ahead. This is the second unique feature of SBSAT. Other solvers perform either depth-first look-ahead, also known as restarts, or breadth-first look-ahead, such as in Prover. Since, as was mentioned earlier, many problems are hard because they do not reveal inferences until deep in the search, the function-complete look-ahead approach appears to have an enhanced potential for discovery of at least some of these hard-to-get inferences. SBSAT remains under development and currently serves as a testbed for several new approaches to solving difficult instances of Satisfiability.

When contaminated sites are drained by aquifers, remediation plans must include an effective means to intercept and extract a sufficient volume of contaminant from groundwater systems near the site to prevent unsatisfactory concentrations from accumulating at other sites served by these systems. The kinds of interception equipment available include injection wells, extractions wells, and trenches. Injection wells pump water into the ground and are used to control locally the direction of groundwater and therefore the flow of contaminant. Extraction wells are used to pump contaminated water out of the ground. Trenches provide a passive means for contaminant extraction and may be an attractive alternative to extraction wells in certain cases.

The optimal placement of these remediation objects is a complex function of many variables such as local knowledge, capital and operating costs of the remediation objects, availability of remediation object resources, what are considered safe levels of contaminant concentration, what can or must be done with the recovered contaminated water, and several others. This level of complexity requires some mechanical computational assistance. However, although the flow of contaminant through a groundwater system remediated by a particular extraction system can be simulated by a computer, there was no computer aid which finds an optimal or near optimal recovery plan: that is, a plan which recovers sufficient contaminant at least cost.

Some of the features of our software are:

It was available on DOS machines and MacIntosh computers.

It could be used in the classroom to assist in the teaching of groundwater principles.

It could mix approximation algorithms for optimization with simulation algorithms for validation. As such, it could be a research platform for experimenting with a variety of optimization techniques.

It could provide several levels of simulation and approximation accuracy: the final remediation plan for a site could be determined by the process of stepwise-refinement through several levels.

It could provide several levels of output detail. For example, one may view the status of the entire site at one particular time in order to understand global, spatial relationships, or view specific information at a point on the site in order to understand time dependent relationships between measurable attributes. Windows and dialog boxes provide the output. These may be opened and closed easily when needed.

Many of the attributes of the simulation could be represented visually. A model of a site could be represented on the computer screen. Site features such as roads, buildings, and rivers could be visible or invisible as needed. Soil properties such as permeability could be represented visually. Quantities such as Head, and Concentration could also be represented visually using color shading. Remediation objects could be moved around the screen under mouse control and automatically by the results of intrinsic approximation algorithms; in this way, partial results could be observed rapidly, possibly leading to abandonment of some alternatives in favor of others. Here is a screenshot:



It could solve a variety of subsurface transport problems using a variety of treatment technologies. Thus, the cost effectiveness of various methods of treatment could be compared.

The most important feature of the program was the ability to integrate different kinds of information at different levels of detail. The user was able to concentrate on site visualization and specific quantities at the same time, as needed. For example, a user could locate a test-point on the visualized landscape and pop open a graph showing the history of an attribute at that point. Then the user could explore that graph with the mouse to find exact values at particular graph points.