Logic-based decision support. Mixed integer model formulation (Q1210858)

Traditionally, research fields as integer programming and automated theorem proving were quite separate disciplines and few researchers were active in both of them. While integer programming mainly belongs to operations research, automated theorem proving is rather a part of mathematical logic. But in this book, a bridge connecting these two disciplines is built. The text is divided into two main parts: (1) mixed integer programming, and (2) logical decision methods based on theorem proving methods. The central concept of the first part is bounded mixed integer programming representability (b-MIP representability); here sets \(S\subseteq {\mathbb{R}}^ n\) are represented by (A,B,h) such that \(x\in S\) if and only if \(Ax+By\geq h\) for some binary vector y of auxiliary variables (A,B are matrices; x,y,h vectors). b-MIP representability is further characterized by representability as finite union of polyhedra having the same recession cone. Moreover techniques are developed to represent sets defined by intersections, Cartesian products, sums, unions and combinations of these operations. In the second part of the book, a link between propositional logic and integer programming is defined; it is shown how the propositional satisfiability for clause forms can be represented by a system of inequalities. The technique is the following: To every propositional variable X we assign a binary variable z(X); for \(\neg X\) we set \(z(\neg X)=1-z(X)\). Thus, when \(C=L_ 1\vee...\vee L_ n\) is a clause, we represent it by the inequality \(z(L_ n)+...+z(L_ n)\geq 1\) (the meaning is: ``C is true''). Determining satisfiability of a set of clauses then becomes the problem of finding whether the set described by the corresponding inequalities is nonempty. Some statistical time tables show extremely good results for some types of large clause sets. As logical technique to decide satisiability of propositional clause sets the method of Davis and Putnam is discussed as well as its reduced form for Horn clause sets (there is no splitting rule). The book also presents a nice, if not very detailed, survey of propositional and predicate logic. It is a very good choice to introduce a Gentzen-type system (natural deduction) instead of a Hilbert-type one. Besides this introductory material the book contains many important results from logical complexity theory (unfortunately without proofs) such as the exponential time complexity of the \(\forall\)-class, the superexponentiality of Presburger arithmetic and the polynomial time hierarchy. For the (decidable) \(\forall^*\)- and \(\exists^*\)-classes projections to propositional logic are given; to the propositional forms b-MIP.r techniques are applied again. Logical and b-MIP.r methods are combined to handle a kind of mixed structure, that are models of the form \(M=(X,D,W,P_ 1,...,P_ S)\) where \(X\subseteq {\mathbb{R}}^ n\), D is a domain, \(W\subseteq X\times D\) and \(P_ i\) are predicates on W. These structures are proposed to handle problems having a numerical as well as a logical component. The last chapter of the book gives an outlock of the (possible) convergence of operations research and computational logic in the future. The book contains an impressive wealth of results; however few of them are also proved in the book. That means the reader is forced to read a lot of literature cited in the references. Thus, in order to make the book self-contained, the addition of some proofs would be quite helpful. The term ``testable'' instead of ``decidable'' is rather erroneous (in the chapter on computational complexity) and should be avoided. Güdel, Schütte and Löwenheim should not be written as Godel, Schutte, Lowenheim, but instead (in case there are no ``ö''s and ``ü''s available) as Goedel, Schuette, Loewenheim. In spite of some weak points indicated above and of some minor formal errors this book contains many creative ideas on interdisciplinary research, which may prove very effective in the future. People interested in operations research and/or theorem proving should read this very stimulating book.