Constraint-Based Reasoning
Multiple Metric Learning for Structured Data
We address the problem of merging graph and feature-space information while learning a metric from structured data. Existing algorithms tackle the problem in an asymmetric way, by either extracting vectorized summaries of the graph structure or adding hard constraints to feature-space algorithms. Following a different path, we define a metric regression scheme where we train metric-constrained linear combinations of dissimilarity matrices. The idea is that the input matrices can be pre-computed dissimilarity measures obtained from any kind of available data (e.g. node attributes or edge structure). As the model inputs are distance measures, we do not need to assume the existence of any underlying feature space. Main challenge is that metric constraints (especially positive-definiteness and sub-additivity), are not automatically respected if, for example, the coefficients of the linear combination are allowed to be negative. Both positive and sub-additive constraints are linear inequalities, but the computational complexity of imposing them scales as O(D3), where D is the size of the input matrices (i.e. the size of the data set). This becomes quickly prohibitive, even when D is relatively small. We propose a new graph-based technique for optimizing under such constraints and show that, in some cases, our approach may reduce the original computational complexity of the optimization process by one order of magnitude. Contrarily to existing methods, our scheme applies to any (possibly non-convex) metric-constrained objective function.
Learning Interpretable Models in the Property Specification Language
Roy, Rajarshi, Fisman, Dana, Neider, Daniel
We address the problem of learning human-interpretable descriptions of a complex system from a finite set of positive and negative examples of its behavior. In contrast to most of the recent work in this area, which focuses on descriptions expressed in Linear Temporal Logic (LTL), we develop a learning algorithm for formulas in the IEEE standard temporal logic PSL (Property Specification Language). Our work is motivated by the fact that many natural properties, such as an event happening at every n-th point in time, cannot be expressed in LTL, whereas it is easy to express such properties in PSL. Moreover, formulas in PSL can be more succinct and easier to interpret (due to the use of regular expressions in PSL formulas) than formulas in LTL. Our learning algorithm builds on top of an existing algorithm for learning LTL formulas. Roughly speaking, our algorithm reduces the learning task to a constraint satisfaction problem in propositional logic and then uses a SAT solver to search for a solution in an incremental fashion. We have implemented our algorithm and performed a comparative study between the proposed method and the existing LTL learning algorithm. Our results illustrate the effectiveness of the proposed approach to provide succinct human-interpretable descriptions from examples.
A Constraint Driven Solution Model for Discrete Domains with a Case Study of Exam Timetabling Problems
Many science and engineering applications require finding solutions to planning and optimization problems by satisfying a set of constraints. These constraint problems (CPs) are typically NP-complete and can be formalized as constraint satisfaction problems (CSPs) or constraint optimization problems (COPs). Evolutionary algorithms (EAs) are good solvers for optimization problems ubiquitous in various problem domains, however traditional operators for EAs are 'blind' to constraints or generally use problem dependent objective functions; as they do not exploit information from the constraints in search for solutions. A variation of EA, Intelligent constraint handling evolutionary algorithm (ICHEA), has been demonstrated to be a versatile constraints-guided EA for continuous constrained problems in our earlier works in (Sharma and Sharma, 2012) where it extracts information from constraints and exploits it in the evolutionary search to make the search more efficient. In this paper ICHEA has been demonstrated to solve benchmark exam timetabling problems, a classic COP. The presented approach demonstrates competitive results with other state-of-the-art approaches in EAs in terms of quality of solutions. ICHEA first uses its inter-marriage crossover operator to satisfy all the given constraints incrementally and then uses combination of traditional and enhanced operators to optimize the solution. Generally CPs solved by EAs are problem dependent penalty based fitness functions. We also proposed a generic preference based solution model that does not require a problem dependent fitness function, however currently it only works for mutually exclusive constraints.
Scalable and Probabilistically Complete Planning for Robotic Spatial Extrusion
Garrett, Caelan Reed, Huang, Yijiang, Lozano-Pérez, Tomás, Mueller, Caitlin Tobin
There is increasing demand for automated systems that can fabricate 3D structures. Robotic spatial extrusion has become an attractive alternative to traditional layer-based 3D printing due to a manipulator's flexibility to print large, directionally-dependent structures. However, existing extrusion planning algorithms require a substantial amount of human input, do not scale to large instances, and lack theoretical guarantees. In this work, we present a rigorous formalization of robotic spatial extrusion planning and provide several efficient and probabilistically complete planning algorithms. The key planning challenge is, throughout the printing process, satisfying both stiffness constraints that limit the deformation of the structure and geometric constraints that ensure the robot does not collide with the structure. We show that, although these constraints often conflict with each other, a greedy backward state-space search guided by a stiffness-aware heuristic is able to successfully balance both constraints. We empirically compare our methods on a benchmark of over 40 simulated extrusion problems. Finally, we apply our approach to 3 real-world extrusion problems.
Testing Unsatisfiability of Constraint Satisfaction Problems via Tensor Products
We study the design of stochastic local search methods to prove unsatisfiability of a constraint satisfaction problem (CSP). For a binary CSP, such methods have been designed using the microstructure of the CSP. Here, we develop a method to decompose the microstructure into graph tensors. We show how to use the tensor decomposition to compute a proof of unsatisfiability efficiently and in parallel. We also offer substantial empirical evidence that our approach improves the praxis. For instance, one decomposition yields proofs of unsatisfiability in half the time without sacrificing the quality. Another decomposition is twenty times faster and effective three-tenths of the times compared to the prior method. Our method is applicable to arbitrary CSPs using the well known dual and hidden variable transformations from an arbitrary CSP to a binary CSP.
Tackling Air Traffic Conflicts as a Weighted CSP : Experiments with the Lumberjack Method
Chaboud, Thomas, Pralet, Cédric, Schmidt, Nicolas
In this paper, we present an extension to an air traffic conflicts resolution method consisting in generating a large number of trajectories for a set of aircraft, and efficiently selecting the best compatible ones. We propose a multimanoeuvre version which encapsulates different conflict-solving algorithms, in particular an original "smart brute-force" method and the well-known ToulBar2 CSP toolset. Experiments on several benchmarks show that the first one is very efficient on cases involving few aircraft (representative of what actually happens in operations), allowing us to search through a large pool of manoeuvres and trajectories; however, this method is overtaken by its complexity when the number of aircraft increases to 7 and more. Conversely, within acceptable times, the ToulBar2 toolset can handle conflicts involving more aircraft, but with fewer possible trajectories for each.
Benchmarking Symbolic Execution Using Constraint Problems -- Initial Results
Verma, Sahil, Yap, Roland H. C.
Symbolic execution is a powerful technique for bug finding and program testing. It is successful in finding bugs in real-world code. The core reasoning techniques use constraint solving, path exploration, and search, which are also the same techniques used in solving combinatorial problems, e.g., finite-domain constraint satisfaction problems (CSPs). We propose CSP instances as more challenging benchmarks to evaluate the effectiveness of the core techniques in symbolic execution. We transform CSP benchmarks into C programs suitable for testing the reasoning capabilities of symbolic execution tools. From a single CSP P, we transform P depending on transformation choice into different C programs. Preliminary testing with the KLEE, Tracer-X, and LLBMC tools show substantial runtime differences from transformation and solver choice. Our C benchmarks are effective in showing the limitations of existing symbolic execution tools. The motivation for this work is we believe that benchmarks of this form can spur the development and engineering of improved core reasoning in symbolic execution engines.
Correcting Knowledge Base Assertions
Chen, Jiaoyan, Chen, Xi, Horrocks, Ian, Jimenez-Ruiz, Ernesto, Myklebus, Erik B.
The usefulness and usability of knowledge bases (KBs) is often limited by quality issues. One common issue is the presence of erroneous assertions, often caused by lexical or semantic confusion. We study the problem of correcting such assertions, and present a general correction framework which combines lexical matching, semantic embedding, soft constraint mining and semantic consistency checking. The framework is evaluated using DBpedia and an enterprise medical KB.
Training Neural Network Controllers Using Control Barrier Functions in the Presence of Disturbances
Yaghoubi, Shakiba, Fainekos, Georgios, Sankaranarayanan, Sriram
Control Barrier Functions (CBF) have been recently utilized in the design of provably safe feedback control laws for nonlinear systems. These feedback control methods typically compute the next control input by solving an online Quadratic Program (QP). Solving QP in real-time can be a computationally expensive process for resource constraint systems. In this work, we propose to use imitation learning to learn Neural Network-based feedback controllers which will satisfy the CBF constraints. In the process, we also develop a new class of High Order CBF for systems under external disturbances. We demonstrate the framework on a unicycle model subject to external disturbances, e.g., wind or currents.
A Survey on the Use of Preferences for Virtual Machine Placement in Cloud Data Centers
Alashaikh, Abdulaziz, Alanazi, Eisa, Al-Fuqaha, Ala
With the rapid development of virtualization techniques, cloud data centers allow for cost effective, flexible, and customizable deployments of applications on virtualized infrastructure. Virtual machine (VM) placement aims to assign each virtual machine to a server in the cloud environment. VM Placement is of paramount importance to the design of cloud data centers. Typically, VM placement involves complex relations and multiple design factors as well as local policies that govern the assignment decisions. It also involves different constituents including cloud administrators and customers that might have disparate preferences while opting for a placement solution. Thus, it is often valuable to not only return an optimized solution to the VM placement problem but also a solution that reflects the given preferences of the constituents. In this paper, we provide a detailed review on the role of preferences in the recent literature on VM placement. We further discuss key challenges and identify possible research opportunities to better incorporate preferences within the context of VM placement.