A biased randomized algorithm has been developed to enable the rapid computational solution of a propositional-satisfiability (SAT) problem equivalent to a diagnosis problem. The closest competing methods of automated diagnosis are described in the preceding article "Fast Algorithms for Model- Based Diagnosis" and "Two Methods of Efficient Solution of the Hitting-Set Problem" (NPO-30584), which appears elsewhere in this issue.
It is necessary to recapitulate some of the information from the cited articles as a prerequisite to a description of the present method. As used here, "diagnosis" signifies, more precisely, a type of model-based diagnosis in which one explores any logical inconsistencies between the observed and expected behaviors of an engineering system. The function of each component and the interconnections among all the components of the engineering system are represented as a logical system. Hence, the expected behavior of the engineering system is represented as a set of logical consequences. Faulty components lead to inconsistency between the observed and expected behaviors of the system, represented by logical inconsistencies. Diagnosis — the task of finding the faulty components — reduces to finding the components, the abnormalities of which could explain all the logical inconsistencies. One seeks a minimal set of faulty components (denoted a minimal diagnosis), because the trivial solution, in which all components are deemed to be faulty, always explains all inconsistencies.
In the methods of the cited articles, the minimal-diagnosis problem is treated as equivalent to a minimal-hitting-set problem, which is translated from a combinatorial to a computational problem by mapping it onto the Boolean-satisfiability and integer-programming problems. The integer-programming approach taken in one of the prior methods is complete (in the sense that it is guaranteed to find a solution if one exists) and slow and yields a lower bound on the size of the minimal diagnosis. In contrast, the present approach is incomplete and fast and yields an upper bound on the size of the minimal diagnosis.
The encoding of the diagnosis problem as an SAT problem for the purpose of the present method is basically the same as the encoding of the diagnosis problem as a hitting-set problem in the methods of the cited articles. In the present case, one seeks a minimal solution to the SAT problem — that is, a solution in which the fewest variables are set to TRUE. In a typical prior local-search algorithm for solving the SAT problem, one guesses at a complete solution and then, through a sequence of partly random and partly greedy flips, tries to adjust the guess to reduce the number of unsatisfied clauses while increasing, or leaving unchanged, the number of satisfied clauses. Eventually, one converges toward a complete solution. Although such local-search algorithms are not complete, in practice, they outperform other algorithms for solving the SAT problem.
The prior local-search algorithms used to solve the SAT problem sometimes flounder in the search space without converging to the solution, making it necessary to restart the algorithms from time to time. Usually, in such a case, one randomly assigns a value of TRUE or FALSE to each variable in the SAT problem. In the present algorithm, one biases this otherwise random assignment toward FALSE in the effort to make the subsequent random and greedy flips lead to a solution in which the fewest variables are TRUE. Hence, one increases the probability of reaching a minimal solution. If the solution is not a minimal diagnosis, it is nevertheless guaranteed to provide an upper bound on the minimal diagnosis, and thereby to be useful as a guide to the use of other diagnostic algorithms.
This work was done by Colin Williams and Farrokh Vartan of Caltech for NASA's Jet Propulsion Laboratory. For further information, access the Technical Support Package (TSP) free on-line at www.techbriefs.com/tsp under the Information Sciences category.
This Brief includes a Technical Support Package (TSP).
Biased Randomized Algorithm for Fast Model-Based Diagnosis
(reference NPO-40065) is currently available for download from the TSP library.
Don't have an account? Sign up here.