Effective logic computation

Preface......Page 13 1.1 Overview......Page 16 1.2 History......Page 20 1.3 Logic Problems......Page 22 1.4 Prior Results......Page 24 1.5 Overall Approach......Page 32 1.6 Reading Guide......Page 35 2.2 Sets......Page 37 2.3 Propositional Logic......Page 38 2.4 First-Order Logic......Page 46 2.5 Graphs......Page 48 2.6 Matrices......Page 64 2.7 Complexity of Algorithms......Page 82 2.8 References......Page 83 3.1 Overview......Page 84 3.2 Definitions......Page 85 3.3 Minor......Page 92 3.4 Connectivity......Page 95 3.5 Finding Separations......Page 97 3.6 Sums......Page 116 3.7 Extensions and References......Page 121 4.1 Overview......Page 123 4.2 Basic Equations and Inequalities......Page 124 4.3 System B and Linear Algebra......Page 127 4.4 B-Independence System......Page 148 4.5 Connectivity......Page 156 4.6 Finding Separations......Page 160 4.7 Sums......Page 167 4.8 A Glimpse Ahead......Page 173 4.9 D-System......Page 175 4.10 Extensions and References......Page 181 5.1 Overview......Page 185 5.2 Centrality......Page 187 5.3 Properties of Centrality......Page 190 5.4 2SAT Matrices......Page 196 5.5 Nearly Negative Matrices......Page 202 5.6 Hidden Nearly Negative Matrices......Page 205 5.7 Balanced Matrices......Page 213 5.8 Comparison of Matrix Classes......Page 231 5.9 Extensions and References......Page 236 6.1 Overview......Page 243 6.2 Minimal Excluded Boolean Minors......Page 244 6.3 Minimal Excluded Subregions......Page 259 6.4 References......Page 269 7.1 Overview......Page 271 7.2 Definitions......Page 275 7.3 Characterizations......Page 277 7.4 Properties......Page 285 7.5 Algorithms......Page 290 7.6 Extensions......Page 296 8.1 Overview......Page 297 8.2 Algorithm for SAT and MINSAT......Page 300 8.3 Heuristic for Integer Programs......Page 306 8.4 Decomposition for 2SAT......Page 312 8.5 Decomposition for Hidden Near Negativity......Page 315 8.6 Decomposition for Network Property......Page 318 8.7 Extensions and References......Page 322 9.1 Overview......Page 328 9.2 Definitions and Properties......Page 329 9.3 Decomposition Algorithm......Page 332 9.4 Solution Algorithm......Page 337 9.5 Extensions and References......Page 342 10.1 Overview......Page 345 10.2 Review and Definitions......Page 346 10.3 Decomposition Algorithms......Page 349 10.4 Solution Algorithm......Page 356 10.5 Extensions......Page 363 11.1 Overview......Page 365 11.2 Definitions......Page 366 11.3 Decomposition Algorithm......Page 371 11.4 Solution Algorithm......Page 375 11.5 Extensions and References......Page 382 12.1 Overview......Page 384 12.2 Definitions......Page 385 12.3 Decomposition Algorithms......Page 391 12.4 Solution Algorithm......Page 396 12.5 Extensions......Page 406 13.1 Overview......Page 409 13.2 Structure of Solution Algorithms......Page 410 13.3 Algorithm for Component Matrix......Page 412 13.4 Analysis Algorithm......Page 416 13.5 Approximate Minimization......Page 429 13.6 Pre- and Postprocessing......Page 432 13.7 Extensions and References......Page 436 14.2 Review of Centrality and Semicentrality Results......Page 437 14.3 Construction of Central and Semicentral Classes......Page 441 14.4 Link to Analysis Algorithm......Page 443 14.5 Extensions and References......Page 445 References......Page 446 Author Index......Page 466 Subject Index......Page 472 Preface 13 Chapter 1 Introduction 16 1.1 Overview 16 1.2 History 20 1.3 Logic Problems 22 1.4 Prior Results 24 1.5 Overall Approach 32 1.6 Reading Guide 35 Chapter 2 Basic Concepts 37 2.1 Overview 37 2.2 Sets 37 2.3 Propositional Logic 38 2.4 First-Order Logic 46 2.5 Graphs 48 2.6 Matrices 64 2.7 Complexity of Algorithms 82 2.8 References 83 Chapter 3 Some Matroid Theory 84 3.1 Overview 84 3.2 Definitions 85 3.3 Minor 92 3.4 Connectivity 95 3.5 Finding Separations 97 3.6 Sums 116 3.7 Extensions and References 121 Chapter 4 System B, Linear Algebra, and Matroids 123 4.1 Overview 123 4.2 Basic Equations and Inequalities 124 4.3 System B and Linear Algebra 127 4.4 B-Independence System 148 4.5 Connectivity 156 4.6 Finding Separations 160 4.7 Sums 167 4.8 A Glimpse Ahead 173 4.9 D-System 175 4.10 Extensions and References 181 Chapter 5 Special Matrix Classes 185 5.1 Overview 185 5.2 Centrality 187 5.3 Properties of Centrality 190 5.4 2SAT Matrices 196 5.5 Nearly Negative Matrices 202 5.6 Hidden Nearly Negative Matrices 205 5.7 Balanced Matrices 213 5.8 Comparison of Matrix Classes 231 5.9 Extensions and References 236 Chapter 6 Characterizations of Hidden Near Negativity 243 6.1 Overview 243 6.2 Minimal Excluded Boolean Minors 244 6.3 Minimal Excluded Subregions 259 6.4 References 269 Chapter 7 Boolean Closed Matrices 271 7.1 Overview 271 7.2 Definitions 275 7.3 Characterizations 277 7.4 Properties 285 7.5 Algorithms 290 7.6 Extensions 296 Chapter 8 Closed Subregion Decomposition 297 8.1 Overview 297 8.2 Algorithm for SAT and MINSAT 300 8.3 Heuristic for Integer Programs 306 8.4 Decomposition for 2SAT 312 8.5 Decomposition for Hidden Near Negativity 315 8.6 Decomposition for Network Property 318 8.7 Extensions and References 322 Chapter 9 Monotone Sum 328 9.1 Overview 328 9.2 Definitions and Properties 329 9.3 Decomposition Algorithm 332 9.4 Solution Algorithm 337 9.5 Extensions and References 342 Chapter 10 Closed Sum 345 10.1 Overview 345 10.2 Review and Definitions 346 10.3 Decomposition Algorithms 349 10.4 Solution Algorithm 356 10.5 Extensions 363 Chapter 11 Augmented Sum 365 11.1 Overview 365 11.2 Definitions 366 11.3 Decomposition Algorithm 371 11.4 Solution Algorithm 375 11.5 Extensions and References 382 Chapter 12 Linear Sum 384 12.1 Overview 384 12.2 Definitions 385 12.3 Decomposition Algorithms 391 12.4 Solution Algorithm 396 12.5 Extensions 406 Chapter 13 Analysis Algorithm 409 13.1 Overview 409 13.2 Structure of Solution Algorithms 410 13.3 Algorithm for Component Matrix 412 13.4 Analysis Algorithm 416 13.5 Approximate Minimization 429 13.6 Pre- and Postprocessing 432 13.7 Extensions and References 436 Chapter 14 Central and Semicentral Classes 437 14.1 Overview 437 14.2 Review of Centrality and Semicentrality Results 437 14.3 Construction of Central and Semicentral Classes 441 14.4 Link to Analysis Algorithm 443 14.5 Extensions and References 445 References 446 Author Index 466 Subject Index 472