Approved for public release; distribution is unlimited. / This thesis presents a formal analysis process and the results of applying that process to the MLS LAN: TCB-to- TCBE, Session Status, and TCBE-to-Session Server Protocols. The formal analysis process consists of several distinct stages: the creation of a detailed informal protocol description, analyzing that description to reveal assumptions and areas of interest not directly addressed in the protocol description, the transformation of that description and the related assumptions into a formal Strand Space representation, analyzing that representation to reveal assumptions and areas of interest, and concluding with an application of John Millen's automated Constraint Checker analysis tool to the Strand Space representations under an extremely limited set of conditions to prove certain protocol secrecy properties.

Yau Po Chung. / Thesis (M.Phil.)--Chinese University of Hong Kong, 1998. / Includes bibliographical references (leaves 91-92). / Abstract also in Chinese. / Chapter 1 --- Introduction --- p.1 / Chapter 2 --- Background --- p.3 / Chapter 2.1 --- Temporal Theories --- p.3 / Chapter 2.2 --- Related Works --- p.4 / Chapter 2.2.1 --- Consistency and Satisfiability of Timing Specifications --- p.4 / Chapter 2.2.2 --- Symbolic Constraint Satisfaction --- p.5 / Chapter 3 --- Previous Developed Work --- p.7 / Chapter 3.1 --- Previous Problem Domain --- p.7 / Chapter 3.1.1 --- Basics of MC68000 Read Cycle --- p.7 / Chapter 3.2 --- Knowledge-based System Structure --- p.9 / Chapter 3.3 --- Diagnostic Reasoning Mechanisms --- p.10 / Chapter 3.4 --- Time Range Approach --- p.11 / Chapter 3.4.1 --- Time Range Representation --- p.11 / Chapter 3.4.2 --- Constraint Satisfaction of Time Ranges --- p.12 / Chapter 3.4.3 --- Constraint Propagation of Time Ranges --- p.13 / Chapter 3.5 --- Fuzzy Time Point Approach --- p.14 / Chapter 3.5.1 --- Fuzzy Time Point Models --- p.14 / Chapter 3.5.2 --- Definition of Fuzzy Time Points --- p.15 / Chapter 3.5.3 --- Constraint Propagation of Fuzzy Time Points --- p.17 / Chapter 3.5.4 --- Constraint Satisfaction of Fuzzy Time Points --- p.18 / Chapter 4 --- The Proposed Segmented Time Range Approach --- p.20 / Chapter 4.1 --- Introduction --- p.20 / Chapter 4.2 --- The Insufficiency of The Existing Time Range Approach --- p.22 / Chapter 4.3 --- Segmented Time Range Approach --- p.23 / Chapter 4.3.1 --- The Representation --- p.23 / Chapter 4.3.2 --- Constraint Propagation and Satisfaction --- p.25 / Chapter 4.3.3 --- Contributions --- p.25 / Chapter 4.3.4 --- Limitations --- p.29 / Chapter 4.4 --- Conclusion --- p.30 / Chapter 5 --- New Problem Domain and Our New System --- p.31 / Chapter 5.1 --- Introduction --- p.31 / Chapter 5.2 --- Pentium-SRAM Interfacing Problem --- p.31 / Chapter 5.2.1 --- Asynchronous SRAM Solution --- p.32 / Chapter 5.2.2 --- Synchronous SRAM Solution --- p.33 / Chapter 5.3 --- The Knowledge Base --- p.35 / Chapter 5.4 --- Characteristics of Our New System --- p.35 / Chapter 6 --- Burst Read Cycle --- p.37 / Chapter 6.1 --- Introduction --- p.37 / Chapter 6.2 --- Asynchronous SRAM Solution --- p.37 / Chapter 6.2.1 --- Implementation --- p.39 / Chapter 6.2.2 --- Implementation Results --- p.45 / Chapter 6.3 --- Synchronous SRAM Solution --- p.48 / Chapter 6.3.1 --- Implementation --- p.49 / Chapter 6.3.2 --- Implementation Results --- p.56 / Chapter 6.4 --- Conclusion --- p.58 / Chapter 7 --- Burst Write Cycle --- p.60 / Chapter 7.1 --- Introduction --- p.60 / Chapter 7.2 --- Asynchronous SRAM Solution --- p.60 / Chapter 7.2.1 --- Implementation --- p.61 / Chapter 7.2.2 --- Implementation Results --- p.67 / Chapter 7.3 --- Synchronous SRAM Solution --- p.71 / Chapter 7.3.1 --- Implementation --- p.71 / Chapter 7.3.2 --- Implementation Results --- p.79 / Chapter 7.4 --- Conclusion --- p.82 / Chapter 8 --- Conclusion --- p.83 / Chapter 8.1 --- Summary of Achievements --- p.83 / Chapter 8.2 --- Future Development --- p.86 / Appendix Some Characteristics of Our New System --- p.89 / Bibliography --- p.91

by Choi Mo Fung Kenneth. / Thesis (M.Phil.)--Chinese University of Hong Kong, 1998. / Includes bibliographical references (leaves 105-112). / Abstract also in Chinese. / Chapter 1 --- Introduction --- p.1 / Chapter 1.1 --- Constraint Satisfaction Problems --- p.2 / Chapter 1.2 --- Constraint Satisfaction Techniques --- p.2 / Chapter 1.3 --- Motivation of the Research --- p.4 / Chapter 1.4 --- Overview of the Thesis --- p.5 / Chapter 2 --- Related Work --- p.7 / Chapter 2.1 --- Min-conflicts Heuristic --- p.7 / Chapter 2.2 --- GSAT --- p.8 / Chapter 2.3 --- Breakout Method --- p.8 / Chapter 2.4 --- GENET --- p.9 / Chapter 2.5 --- E-GENET --- p.9 / Chapter 2.6 --- DLM --- p.10 / Chapter 2.7 --- Simulated Annealing --- p.11 / Chapter 2.8 --- Genetic Algorithms --- p.12 / Chapter 2.9 --- Tabu Search --- p.12 / Chapter 2.10 --- Integer Programming --- p.13 / Chapter 3 --- Background --- p.15 / Chapter 3.1 --- GENET --- p.15 / Chapter 3.1.1 --- Network Architecture --- p.15 / Chapter 3.1.2 --- Convergence Procedure --- p.18 / Chapter 3.2 --- Classical Optimization --- p.22 / Chapter 3.2.1 --- Optimization Problems --- p.22 / Chapter 3.2.2 --- The Lagrange Multiplier Method --- p.23 / Chapter 3.2.3 --- Saddle Point of Lagrangian Function --- p.25 / Chapter 4 --- Binary CSP's as Zero-One Integer Constrained Minimization Prob- lems --- p.27 / Chapter 4.1 --- From CSP to SAT --- p.27 / Chapter 4.2 --- From SAT to Zero-One Integer Constrained Minimization --- p.29 / Chapter 5 --- A Continuous Lagrangian Approach for Solving Binary CSP's --- p.33 / Chapter 5.1 --- From Integer Problems to Real Problems --- p.33 / Chapter 5.2 --- The Lagrange Multiplier Method --- p.36 / Chapter 5.3 --- Experiment --- p.37 / Chapter 6 --- A Discrete Lagrangian Approach for Solving Binary CSP's --- p.39 / Chapter 6.1 --- The Discrete Lagrange Multiplier Method --- p.39 / Chapter 6.2 --- Parameters of CSVC --- p.43 / Chapter 6.2.1 --- Objective Function --- p.43 / Chapter 6.2.2 --- Discrete Gradient Operator --- p.44 / Chapter 6.2.3 --- Integer Variables Initialization --- p.45 / Chapter 6.2.4 --- Lagrange Multipliers Initialization --- p.46 / Chapter 6.2.5 --- Condition for Updating Lagrange Multipliers --- p.46 / Chapter 6.3 --- A Lagrangian Reconstruction of GENET --- p.46 / Chapter 6.4 --- Experiments --- p.52 / Chapter 6.4.1 --- Evaluation of LSDL(genet) --- p.53 / Chapter 6.4.2 --- Evaluation of Various Parameters --- p.55 / Chapter 6.4.3 --- Evaluation of LSDL(max) --- p.63 / Chapter 6.5 --- Extension of LSDL --- p.66 / Chapter 6.5.1 --- Arc Consistency --- p.66 / Chapter 6.5.2 --- Lazy Arc Consistency --- p.67 / Chapter 6.5.3 --- Experiments --- p.70 / Chapter 7 --- Extending LSDL for General CSP's: Initial Results --- p.77 / Chapter 7.1 --- General CSP's as Integer Constrained Minimization Problems --- p.77 / Chapter 7.1.1 --- Formulation --- p.78 / Chapter 7.1.2 --- Incompatibility Functions --- p.79 / Chapter 7.2 --- The Discrete Lagrange Multiplier Method --- p.84 / Chapter 7.3 --- A Comparison between the Binary and the General Formulation --- p.85 / Chapter 7.4 --- Experiments --- p.87 / Chapter 7.4.1 --- The N-queens Problems --- p.89 / Chapter 7.4.2 --- The Graph-coloring Problems --- p.91 / Chapter 7.4.3 --- The Car-Sequencing Problems --- p.92 / Chapter 7.5 --- Inadequacy of the Formulation --- p.94 / Chapter 7.5.1 --- Insufficiency of the Incompatibility Functions --- p.94 / Chapter 7.5.2 --- Dynamic Illegal Constraint --- p.96 / Chapter 7.5.3 --- Experiments --- p.97 / Chapter 8 --- Concluding Remarks --- p.100 / Chapter 8.1 --- Contributions --- p.100 / Chapter 8.2 --- Discussions --- p.102 / Chapter 8.3 --- Future Work --- p.103 / Bibliography --- p.105

Thesis (M.S.)--University of Texas at El Paso, 2008. / Title from title screen. Vita. CD-ROM. Includes bibliographical references. Also available online.

Thesis (M.S.)--Georgia State University, 2005. / Title from title screen. Raj Sunderraman, committee chair; Anu G. Bourgeois, Yanqing Zhang, committee members. Electronic text (92 p. : ill. (some col.)) : digital, PDF file. Description based on contents viewed May 25, 2007. Includes bibliographical references (p. 57-58).

Backtracking CSP solvers provide a powerful framework for search and reasoning. The aim of constraint learning is increase global reasoning power by learning new constraints to boost reasoning and hopefully reduce search effort. In this thesis constraint learning is developed in several ways to make it faster and more powerful. First, lazy explanation generation is introduced, where explanations are generated as needed rather than continuously during propagation. This technique is shown to be effective is reducing the number of explanations generated substantially and consequently reducing the amount of time taken to complete a search, over a wide selection of benchmarks. Second, a series of experiments are undertaken investigating constraint forgetting, where constraints are discarded to avoid time and space costs associated with learning new constraints becoming too large. A major empirical investigation into the overheads introduced by unbounded constraint learning in CSP is conducted. This is the first such study in either CSP or SAT. Two significant results are obtained. The first is that typically a small percentage of learnt constraints do most propagation. While this is conventional wisdom, it has not previously been the subject of empirical study. The second is that even constraints that do no effective propagation can incur significant time overheads. Finally, the use of forgetting techniques from the literature is shown to significantly improve the performance of modern learning CSP solvers, contradicting some previous research. Finally, learning is generalised to use disjunctions of arbitrary constraints, where before only disjunctions of assignments and disassignments have been used in practice (g-nogood learning). The details of the implementation undertaken show that major gains in expressivity are available, and this is confirmed by a proof that it can save an exponential amount of search in practice compared with g-nogood learning. Experiments demonstrate the promise of the technique.

The Algorithm Selection Problem is to select the most appropriate way for solving a problem given a choice of different ways. Some of the most prominent and successful applications come from Artificial Intelligence and in particular combinatorial search problems. Machine Learning has established itself as the de facto way of tackling the Algorithm Selection Problem. Yet even after a decade of intensive research, there are no established guidelines as to what kind of Machine Learning to use and how. This dissertation presents an overview of the field of Algorithm Selection and associated research and highlights the fundamental questions left open and problems facing practitioners. In a series of case studies, it underlines the difficulty of doing Algorithm Selection in practice and tackles issues related to this. The case studies apply Algorithm Selection techniques to new problem domains and show how to achieve significant performance improvements. Lazy learning in constraint solving and the implementation of the alldifferent constraint are the areas in which we improve on the performance of current state of the art systems. The case studies furthermore provide empirical evidence for the effectiveness of using the misclassification penalty as an input to Machine Learning. After having established the difficulty, we present an effective technique for reducing it. Machine Learning ensembles are a way of reducing the background knowledge and experimentation required from the researcher while increasing the robustness of the system. Ensembles do not only decrease the difficulty, but can also increase the performance of Algorithm Selection systems. They are used to much the same ends in Machine Learning itself. We finally tackle one of the great remaining challenges of Algorithm Selection -- which Machine Learning technique to use in practice. Through a large-scale empirical evaluation on diverse data taken from Algorithm Selection applications in the literature, we establish recommendations for Machine Learning algorithms that are likely to perform well in Algorithm Selection for combinatorial search problems. The recommendations are based on strong empirical evidence and additional statistical simulations. The research presented in this dissertation significantly reduces the knowledge threshold for researchers who want to perform Algorithm Selection in practice. It makes major contributions to the field of Algorithm Selection by investigating fundamental issues that have been largely ignored by the research community so far.

The struggle to model and solve Combinatorial Optimization Problems (COPs) has challenged the development of new approaches to deal with COPs. In one of the front lines of such approaches, Operational Research (OR) and Constraint Programming (CP) optimization techniques are beginning to converge, despite their very different origins. More specifically, Mixed Integer Linear Programming (MILP) and Constraint Logic Programming (CLP) are at the confluence of the OR and the CP fields. This thesis summarizes and contrasts the essential characteristics of MILP and CLP, and the ways that they can be fruitfully combined. Chapters 1 to 3 sketch the intellectual background for recent efforts at integration and the main results achieved. In addition, these chapters highlight that CLP is known by its reach modeling framework, and the MILP modeling vocabulary is just based on inequalities, which makes the modeling process hard and error-prone. Therefore, a combined CLP-MILP approach suffers from this MILP inherited drawback. In chapter 4, this issue is addressed, and some "high-level" MILP modeling structures based on logical inference paradigms are proposed. These structures help the formulation of MILP models, and can be seen as a contribution towards a unifying modeling framework for a combined CLP-MILP approach. In addition, chapter 5 presents an MILP formulation addressing a combinatorial problem. This problem is focused on issues regarding the oil industry, more specifically, issues involving the scheduling of operational activities in a multi-product pipeline. Chapter 5 demonstrates the applicability of the high-level MILP modeling structures in a real-world scenario. Furthermore, chapter 6 presents a CLP-MILP formulation addressing the same scheduling problem previously exploited. This chapter demonstrates the applicability of the high-level MILP modeling structures in an integrated CLP-MILP modeling framework. The set of simulations conducted indicates that the combined CLP-MILP model was solved to optimality faster than either the MILP model or the CLP model. Thus, the CLP-MILP framework is a promising alternative to deal with the computational burden of this pipeline-scheduling problem. In essence, this thesis considers the integration of CLP and MILP in a modeling standpoint: it conveys the fundamentals of both techniques and the modeling features that help establish a combined CLP-MILP approach. Herein, the concentration is on the building of MILP and CLP-MILP models rather than on the solution process.

The struggle to model and solve Combinatorial Optimization Problems (COPs) has challenged the development of new approaches to deal with COPs. In one of the front lines of such approaches, Operational Research (OR) and Constraint Programming (CP) optimization techniques are beginning to converge, despite their very different origins. More specifically, Mixed Integer Linear Programming (MILP) and Constraint Logic Programming (CLP) are at the confluence of the OR and the CP fields. This thesis summarizes and contrasts the essential characteristics of MILP and CLP, and the ways that they can be fruitfully combined. Chapters 1 to 3 sketch the intellectual background for recent efforts at integration and the main results achieved. In addition, these chapters highlight that CLP is known by its reach modeling framework, and the MILP modeling vocabulary is just based on inequalities, which makes the modeling process hard and error-prone. Therefore, a combined CLP-MILP approach suffers from this MILP inherited drawback. In chapter 4, this issue is addressed, and some "high-level" MILP modeling structures based on logical inference paradigms are proposed. These structures help the formulation of MILP models, and can be seen as a contribution towards a unifying modeling framework for a combined CLP-MILP approach. In addition, chapter 5 presents an MILP formulation addressing a combinatorial problem. This problem is focused on issues regarding the oil industry, more specifically, issues involving the scheduling of operational activities in a multi-product pipeline. Chapter 5 demonstrates the applicability of the high-level MILP modeling structures in a real-world scenario. Furthermore, chapter 6 presents a CLP-MILP formulation addressing the same scheduling problem previously exploited. This chapter demonstrates the applicability of the high-level MILP modeling structures in an integrated CLP-MILP modeling framework. The set of simulations conducted indicates that the combined CLP-MILP model was solved to optimality faster than either the MILP model or the CLP model. Thus, the CLP-MILP framework is a promising alternative to deal with the computational burden of this pipeline-scheduling problem. In essence, this thesis considers the integration of CLP and MILP in a modeling standpoint: it conveys the fundamentals of both techniques and the modeling features that help establish a combined CLP-MILP approach. Herein, the concentration is on the building of MILP and CLP-MILP models rather than on the solution process.

The modal satisfiability problem has to date been solved using either a specifically designed algorithm, or by translating the modal logic formula into a different class of problem, such as a first-order logic, a propositional satisfiability problem or a constraint satisfaction problem. These approaches and the solvers developed to support them are surveyed and a synthesis thereof is presented. The translation of a modal K formula into a constraint satisfaction problem, as developed by Brand et al. [18], is further enhanced. The modal formula, which must be in conjunctive normal form, is translated into layered propositional formulae. Each of these layers is translated into a constraint satisfaction problem and solved using the constraint solver ECLiPSe. I extend this translation to deal with reflexive and transitive accessibility relations, thereby providing for the modal logics KT and S4. Two of the difficulties that arise when these accessibility relations are added are that the resultant formula increases considerably in complexity, and that it is no longer in conjunctive normal form (CNF). I eliminate the need for the conversion of the formula to CNF and deal instead with formulae that are in negation normal form (NNF). I apply a number of enhancements to the formula at each modal layer before it is translated into a constraint satisfaction problem. These include extensive simplification, the assignment of a single value to propositional variables that occur only positively or only negatively, and caching the status of the formula at each node of the search tree. All of these significantly prune the search space. The final results I achieve compare favorably with those obtained by other solvers. / Computing / M.Sc. (Computer Science)