Decomposable structures, Boolean function
representations, and optimization.
Kungliga Tekniska Hogskolan
NADA, S-100 44 Stockholm, Sverige
Abstract. We show the connection between the theory of bounded treewidth graphs, monadic second order definable structures and sets, and boolean decision diagrams. We survey recent results in algorithms for bounded treewidth, symbolic model checking and representation schemes for Boolean functions. Some practical applications are indicated.
This is a survey of a theory of tree-like graphs and other structures. Many aspects of the corresponding method have been known and practised in operations research, reliability engineering, artificial intelligence, and as special applications of dynamic programming. Problems amenable to solution by the methods are discrete optimization, reliability and dependability problems for complex systems, verification of digital designs and software and reasoning with uncertainty. I want to relate the theory of decomposability or tree-likeness to the BDD and symbolic model checking methods used in circuit and program verification and also to methods designed for reasoning in various applied logics in knowledge systems. In these areas, particularly where unstructured problems are solved, it is difficult to formulate a model and to prepare corresponding inputs to optimization programs. One solution to this problem could be the adoption by practitioners of relatively simple logical notations based on second order logic and high-level definition facilities. Similar developments have already taken place in circuit verification.
Since a complete exposition of this problem area will not fit into the present page allowance, we emphasize those aspects that fit in nicely with the presentation strategy and those that seem the most useful in applications. For a very careful and complete exposition, see the series of papers and surveys on the monadic second order logic of graphs by Bruno Courcelle. A recent bibliography is .
1.1 Signatures and structures
Graphs and other combinatorial objects will be represented as structures. A signature F is a set of sorts and a collection of relation and function constants. A symbol is recognized as either of these. Every relation and function constant