Optimization Methods For Logical Inference WILEY-INTERSCIENCE SERIES IN DISCRETE MATHEMATICS AND OPTIMIZATION ADVISORY EDITORS RONALD L. GRAHAM AT& TLaboratories, Florham Park, New Jersey, U.S.A. JAN KAREL LENSTRA Department of Mathematics and Computer Science, Eindhoven University of Technology, Eindhoven, The Netherlands ROBERT E. TARJAN Princeton University, New Jersey, and NEC Research Institute, Princeton, New Jersey, U.S.A. A complete list of titles in this series appears at the end of this volume. Optimization Methods For Logical Inference Vijay Chandru John Hooker A Wiley-Interscience Publication JOHN WILEY & SONS, INC. New York · Chichester · Weinheim · Brisbane · Singapore · Toronto This book is printed on acid-free paper. © Copyright © 1999 by John Wiley & Sons, Inc. All rights reserved. Published simultaneously in Canada. No part of this publication may be reproduced, stored in a retrieval system or transmitted in any form or by any means, electronic, mechanical, photocopying, recording, scanning or otherwise, except as permitted under Sections 107 or 108 of the 1976 United States Copyright Act, without either the prior written permission of the Publisher, or authorization through payment of the appropriate per-copy fee to the Copyright Clearance Center, 222 Rosewood Drive, Danvers, MA 01923, (978) 750-8400, fax (978) 750- 4744. Requests to the Publisher for permission should be addressed to the Permissions Department, John Wiley & Sons, Inc., 605 Third Avenue, New York, NY 10158-0012, (212) 850-6011, fax (212) 850-6008, E-Mail: [email protected]. For ordering and customer service, call 1-800-CALL WILEY. Library of Congress Cataloging in Publication Data; Chandru, Vijay, 1953- Optimization methods for logical inference / Vijay Chandru, John Hooker. p. cm. — (Wiley-Interscience series in discrete mathematics and optimization) "A Wiley-Interscience publication." Includes bibliographical references. ISBN 0-471-57035-4 (cloth : alk. paper) 1. Combinatorial optimization. 2. Logic, Symbolic and mathematical. I. Hooker, John, 1944- . II. Title. III. Series. QA402.5.C447 1999 519.3—dc21 98-44622 CIP 10 9 8 7 6 5 4 32 To our parents Contents Preface xiii 1 Introduction 1 1.1 Logic and Mathematics: The Twain Shall Meet 3 1.2 Inference Methods for Logic Models 6 1.3 Logic Modeling Meets Mathematical Modeling 7 1.4 The Difficulty of Inference 8 2 Propositional Logic: Special Cases 11 2.1 Basic Concepts of Propositional Logic 13 2.1.1 Formulas 13 2.1.2 Normal Forms 16 2.1.3 Rules 22 2.2 Integer Programming Models 23 2.2.1 Optimization and Inference 25 2.2.2 The Linear Programming Relaxation 27 2.3 Horn Polytopes 31 2.3.1 Horn Resolution 31 2.3.2 The Integer Least Element of a Horn Polytope . .. 34 2.3.3 Dual Integrality of Horn Polytopes 37 2.4 Quadratic and Renamable Horn Systems 41 2.4.1 Satisfiability of Quadratic Systems 42 2.4.2 The Median Characteristic of Quadratic Systems . . 44 2.4.3 Recognizing Renamable Horn Systems 45 2.4.4 Q-Horn Propositions 53 2.5 Nested Clause Systems 55 2.5.1 Nested Propositions: Definition and Recognition . . 55 2.5.2 Maximum Satisfiability of Nested Clause Systems 58 2.5.3 Extended Nested Clause Systems 61 vn viii CONTENTS 2.6 Extended Horn Systems 63 2.6.1 The Rounding Theorem 65 2.6.2 Satisfiability of Extended Horn Systems 69 2.6.3 Verifying Renamable Extended Horn Systems . . .. 70 2.6.4 The Unit Resolution Property 71 2.6.5 Extended Horn Rule Bases 73 2.7 Problems with Integral Polytopes 76 2.7.1 Balanced Problems 78 2.7.2 Integrality and Resolution 81 2.8 Limited Backtracking 87 2.8.1 Maximum Embedded Renamable Horn Systems . .. 89 2.8.2 Hierarchies of Satisfiability Problems 91 2.8.3 Generalized and Split Horn Systems 94 3 Propositional Logic: The General Case 97 3.1 Two Classic Inference Methods 98 3.1.1 Resolution for Propositional Logic 99 3.1.2 A Simple Branching Procedure 101 3.1.3 Branching Rules 103 3.1.4 Implementation of a Branching Algorithm 104 3.1.5 Incremental Satisfiability 106 3.2 Generating Hard Problems 109 3.2.1 Pigeonhole Problems 110 3.2.2 Problems Based on Graphs Ill 3.2.3 Random Problems Hard for Resolution 113 3.2.4 Random Problems Hard for Branching 114 3.3 Branching Methods 116 3.3.1 Branch and Bound 117 3.3.2 Jeroslow-Wang Method 121 3.3.3 Horn Relaxation Method 122 3.3.4 Bounded Resolution Method 123 3.4 Tableau Methods 123 3.4.1 The Simplex Method in Tableau Form 124 3.4.2 Pivot and Complement 128 3.4.3 Column Subtraction 131 3.5 Cutting Plane Methods 133 3.5.1 Resolvents as Cutting Planes 134 3.5.2 Unit Resolution and Rank 1 Cuts 136 3.5.3 A Separation Algorithm for Rank 1 Cuts 143 3.5.4 A Branch-and-Cut Algorithm 144 3.5.5 Extended Resolution and Cutting Planes 148 3.6 Resolution for 0-1 Inequalities 150 CONTENTS ix 3.6.1 Inequalities as Logical Formulas 153 3.6.2 A Generalized Resolution Algorithm 154 3.6.3 Some Examples 157 3.7 A Set-Covering Formulation with Facet Cuts 159 3.7.1 The Set-Covering Formulation 160 3.7.2 Elementary Facets of Satisfiability 164 3.7.3 Resolvent Facets Are Prime Implications 166 3.7.4 A Lifting Technique for General Facets 171 3.8 A Nonlinear Programming Approach 173 3.8.1 Formulation as a Nonlinear Programming Problem 174 3.8.2 An Interior Point Algorithm 175 3.8.3 A Satisfiability Heuristic 176 3.9 Tautology Checking in Logic Circuits 177 3.9.1 The Tautology Checking Problem 177 3.9.2 Solution by Benders Decomposition 179 3.9.3 Logical Interpretation of the Benders Algorithm . . 182 3.9.4 A Nonnumeric Algorithm 185 3.9.5 Implementation Issues 188 3.10 Inference as Projection 189 3.10.1 The Logical Projection Problem 191 3.10.2 Computing Logical Projections by Resolution . . .. 191 3.10.3 Projecting Horn Clauses 193 3.10.4 The Polyhedral Projection Problem 193 3.10.5 Inference by Polyhedral Projection 195 3.10.6 Resolution and Fourier-Motzkin Elimination 196 3.10.7 Unit Resolution and Polyhedral Projection 197 3.10.8 Complexity of Inference by Polyhedral Projection 198 3.11 Other Approaches 199 4 Probabilistic and Related Logics 203 4.1 Probabilistic Logic 205 4.1.1 A Linear Programming Model 206 4.1.2 Sensitivity Analysis 209 4.1.3 Column Generation Techniques 211 4.1.4 Point Values Versus Intervals 216 4.2 Bayesian Logic 218 4.2.1 Possible World Semantics for Bayesian Networks . . 220 4.2.2 Using Column Generation with Benders Decomposition 224 X CONTENTS 4.2.3 Limiting the Number of Independence Constraints . 227 4.3 Dempster-Shafer Theory 235 4.3.1 Basic Ideas of Dempster-Shafer Theory 236 4.3.2 A Linear Model of Belief Functions 239 4.3.3 A Set-Covering Model for Dempster's Combination Rule 240 4.3.4 Incomplete Belief Functions 244 4.3.5 Dempster-Shafer Theory vs. Probabilistic Logic . . . 246 4.3.6 A Modification of Dempster's Combination Rule . . 248 4.4 Confidence Factors in Rule Systems 250 4.4.1 Confidence Factors 251 4.4.2 A Graphical Model of Confidence Factor Calculation 254 4.4.3 Jeroslow's Representability Theorem 259 4.4.4 A Mixed Integer Model for Confidence Factors . . . 262 5 Predicate Logic 267 5.1 Basic Concepts of Predicate Logic 269 5.1.1 Formulas 269 5.1.2 Interpretations 270 5.1.3 Skolem Normal Form 271 5.1.4 Herbrand's Theorem 274 5.2 Partial Instantiation Methods 275 5.2.1 Partial Instantiation 276 5.2.2 A Primal Approach to Avoiding Blockage 278 5.2.3 A Dual Approach to Avoiding Blockage 284 5.3 A Method Based on Hypergraphs 287 5.3.1 A Hypergraph Model for Propositional Logic . . .. 288 5.3.2 Shortest Paths in B-Graphs 290 5.3.3 Extension to Universally Quantified Logic 290 5.3.4 Answering Queries 295 5.4 An Infinite 0-1 Programming Model 295 5.4.1 Infinite Dimensional 0-1 Programming 296 5.4.2 A Compactness Theorem 297 5.4.3 Herbrand Theory and Infinite 0-1 Programs 298 5.4.4 Minimum Solutions 299 5.5 The Logic of Arithmetic 301 5.5.1 Decision Methods for Arithmetic 301 5.5.2 Quantitative Methods for Presburger Real Arithmetic 302 5.5.3 Quantitative Methods for Presburger (Integer) Arithmetic 304