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.

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.

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.

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.

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.

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.

Although exploring alternatives is fundamental to creating better interface designs, current processes for creating alternatives are generally manual, limiting the alternatives a designer can explore. We present Scout, a system that helps designers rapidly explore alternatives through mixed-initiative interaction with high-level constraints and design feedback. Prior constraint-based layout systems use low-level spatial constraints and generally produce a single design. Tosupport designer exploration of alternatives, Scout introduces high-level constraints based on design concepts (e.g.,~semantic structure, emphasis, order) and formalizes them into low-level spatial constraints that a solver uses to generate potential layouts. In an evaluation with 18 interface designers, we found that Scout: (1) helps designers create more spatially diverse layouts with similar quality to those created with a baseline tool and (2) can help designers avoid a linear design process and quickly ideate layouts they do not believe they would have thought of on their own.

This paper introduces epistemic graphs as a generalization of the epistemic approach to probabilistic argumentation. In these graphs, an argument can be believed or disbelieved up to a given degree, thus providing a more fine--grained alternative to the standard Dung's approaches when it comes to determining the status of a given argument. Furthermore, the flexibility of the epistemic approach allows us to both model the rationale behind the existing semantics as well as completely deviate from them when required. Epistemic graphs can model both attack and support as well as relations that are neither support nor attack. The way other arguments influence a given argument is expressed by the epistemic constraints that can restrict the belief we have in an argument with a varying degree of specificity. The fact that we can specify the rules under which arguments should be evaluated and we can include constraints between unrelated arguments permits the framework to be more context--sensitive. It also allows for better modelling of imperfect agents, which can be important in multi--agent applications.

Modern board games are a rich source of interesting and new challenges for combinatorial problems. The game Nmbr9 is a solitaire style puzzle game using polyominoes. The rules of the game are simple to explain, but modelling the game effectively using constraint programming is hard. This abstract presents the game, contributes new generalized variants of the game suitable for benchmarking and testing, and describes a model for the presented variants. The question of the top possible score in the standard game is an open challenge.

To solve hard problems, AI relies on a variety of disciplines such as logic, probabilistic reasoning, machine learning and mathematical programming. Although it is widely accepted that solving real-world problems requires an integration amongst these, contemporary representation methodologies offer little support for this. In an attempt to alleviate this situation, we introduce a new declarative programming framework that provides abstractions of well-known problems such as SAT, Bayesian inference, generative models, and convex optimization. The semantics of programs is defined in terms of first-order structures with semiring labels, which allows us to freely combine and integrate problems from different AI disciplines.