The CRIL-NII Collaborative Meeting on Reasoning about Dynamic Constraint Networks

Propositional merging is the problem of aggregating several propositional logic bases, representing either the beliefs or the goals of several agents, into a single coherent base, representing the opinion of the group. This problem is well studied in AI, with the proposal of practical merging methods, as well as theoretical studies of the expected properties. It was shown in particular that this problem is closely related to AGM belief revision theory. It is clear that it has also close links with social choice theory. And, in this talk, we will focus on these links between propositional merging and social choice theory. We will review how some classical properties of social choice theory translate in this merging framework, and what are they implications. We will focus on the problems of truth tracking (through Condorcet's jury theorem), of Independence of Irrelevant Alternatives, of strategy-proofness, and of unanimity. We will see that some of these properties can be translated in different forms, and we will study if they are satisfied by (all, some or none) merging methods.

In this talk, we explain Copris (Constraint Programming in Scala) system which is developed as a Domain-Specific Language (DSL) for constraint programming embedded in Scala programming language. Copris is designed to help Scala programmers to be able to easily solve Constraint Satisfaction Problems (CSP) and Constraint Optimization Problems (COP), and offers richer description power than existing CSP languages, such as JSR-331, a standardized constraint programming API for Java. Copris also provides a high performance constraint solving since SAT-based constraint solver Sugar is used as its backend. When integrated with Java-based SAT solver, such as Sat4j, the whole system can run on JVM.

Event-sequence testing is an effective black-box testing method to detect elusive failures of event-driven hardware/software. Generating test cases for event-sequence testing is to find a sequence covering array (SCA) in Combinatorial Designs. In this talk, we consider the problem of finding optimal sequence covering arrays by Constraint Programming (CP) and Answer Set Programming (ASP). We first present three CP models from different viewpoints of sequence covering arrays: the na\"{i}ve matrix model, the event-position matrix model, and the incidence matrix model. Particularly, in the incidence matrix model, an SCA can be represented by a (0,1)-matrix called the incidence matrix of the array in which the coverage constraints of the given SCA can be concisely expressed. We then present an ASP program of the incidence matrix model. It is compact and faithfully reflects the original constraints of the incidence matrix model. In our experiments, we were able to significantly improve the previously known bounds for many arrays in Kuhn's benchmark set. Moreover, we succeeded in finding optimal solutions for two arrays.

With recent success of SAT technologies, incremental SAT solving has been an active research topic and applied to a wide range of problems. In this talk, by using the Hamiltonian cycle problem, we show a feasibility study of solving a CSP by incremental SAT solving. To find a Hamiltonian cycle, in a standard way, two kinds of constraints are necessary: one ensures every node is connected and the other ensures every node belongs to a cycle. However, a SAT-encoding of the former constraint needs $n^{3}$ clauses, where $n$ is the number of nodes, and it makes it difficult to solve large instances. Our method starts without encoding this constraint and incrementally refines solutions by adding blocking clauses which partially prevent to generate unconnected cycles. To evaluate our method, we made a comparison with a previously proposed SAT-based method on 497 instances whose numbers of nodes are from 11 to 10000. As a result, our method solved 83 more instances and a solved instance was up to over 10 times larger than one by the compared method.

In this work, we focus on two main topics of constraint satisfaction in Bayesian networks. The first topic is the problem of incorporating soft evidence into Bayesian networks by belief revision, to update the model based on probabilistic estimates of certain events. The second topic is the problem of changing network parameters to satisfy probabilistic query constraints by sensitivity analysis, to update the model based on user feedback and environment changes. In both cases, the problem of model disturbance can be measured by a distance measure defined by Chan and Darwiche in terms of bounding query changes.

Many real world problems involve multiple criteria that should be considered separately and optimized simultaneously. A Multi-Objective Distributed Constraint Optimization Problem (MO-DCOP) is the extension of a mono-objective Distributed Constraint Optimization Problem (DCOP) and a centralized Multi-Objective Constraint Optimization Problem (MO-COP). A DCOP is a fundamental problem that can formalize various applications related to multi-agent cooperation. In a MO-COP, various complete, incomplete and interactive algorithms have been developed. On the other hand, in a MO-DCOP, B-MOMS is the only existing (incomplete) algorithm. In this paper, we develop a novel complete algorithm for MO-DCOP. The characteristics of this algorithm are as follows: (i) it is the first complete algorithm which can guarantee to find a Pareto solution, (ii) it is based on a pseudo-tree, which is a widely used graph structure in complete DCOP algorithms, (iii) it utilizes the simplest and the most widely used classical method to find the Pareto solutions of a Multi-Objective Optimization Problem (MOOP), and (iv) the complexity of this algorithm is determined by the induced width of problem instances. Furthermore, we develop an incomplete algorithm for MO-DCOP which is based on a solution criterion called p-optimality. This algorithm can provide the upper bounds of the absolute/ relative errors of the solution, which can be obtained a priori/posteriori, respectively.

In this short presentation I will review the main issues and the basic concepts at work in the research area known as "knowledge compilation". The focus will be laid on the notions of compilability and knowledge compilation map.

In this talk we present several contributions to Conflict Driven Clause Learning (CDCL), which is one of the key components of modern SAT solvers. First, we propose an extended notion of implication graph containing additional arcs, called inverse arcs. These are obtained by taking into account the satisfied clauses of the formula, which are usually ignored by conflict analysis. Secondly, we present an original adaptation of conflict analysis for dynamic clauses subsumption. Our last contribution demonstrates that clause learning can be exploited at each step of the search process, even if a conflict do not occurs. This last contribution aims to derive new but more powerful reasons leading to the implication of a given literal. For all these contributions, we discuss their possible integration to modern SAT solvers.

Taking the best of SAT (at large) technology for a given class of problems requires usually an expert knowledge of the solver used or to rely on an automatic configuration tool. The former condition is usually not satisfied as soon as the user is not a member of the SAT community, and the latter solution does not help the user to understand what is going on inside the solver. We propose an approach that allows the end users of Sat4j to configure a solver for a specific instance. Such an approach is based on both the ability to change dynamically the main settings of the solver when it is running and to display to the user several metrics that inform her about the state of the search in the solver. While the latter has been already explored in the SAT community, and the former has been explored in the constraint programming community, we believe that the combination of that two features is quite unique for SAT solvers. We believe that such a tool could also be used in the classroom to help students to understand how CDCL solvers work.

We study inference and learning of logic-based dynamic systems including Boolean networks (BNs) and cellular automata (CAs). We first show that these systems can be expressed as normal logic programs (NLPs), which are regarded as sets of state transition rules. On the inference side, the supported model semantics of NLPs can characterize point attractors of BNs, and supported classes of NLPs represent periodic oscillation induced by the T_P operator, which can characterize cycle attractors of BNs. On the leaning side, given a set of pairs of interpretations (I,J) such that J=T_P(I), we infer the program P. This framework can be applied to infer BNs from basins of attraction and to identify CAs by observing transitions of configurations.

Soft constraints are useful for treating over-constrained problems that naturally arise in real-life applications. We have been working on frameworks and algorithms for soft constraints to explore their power. In this talk, we present some of our results on constraint hierarchies, semiring-based CSPs, and probabilistic CSPs.

In this talk, we consider non-monotone dualization (NMD) of general Boolean functions from the viewpoint of monotone dualization (MD). We first show that any NMD can be reconstructed into two equivalent MD problems. We then investigate NMD subclasses equivalent to MD based on this reduction technique.

In this talk, we explore some formalisms that can be used to reason about agents's capabilities. More precisely, we look at logics created with the aim of expressing the sentence 'there is an action A by group of agents G after which consequence P is true'. We will see formalisms containing actions with factual effects as well as epistemic effects. That is, we will see formalisms wherein actions may change the environment inhabited by the agents as well as what agents know about this environment. We compare their properties, their expressivity and also the computational complexity of model-checking and satisfiability problems.

This talk will give a short introduction to WCSP (Weighted Constraint Satisfaction Problem) and the soft local consistencies that are widely used. Then, a new algorithm (presented at CP'12) for maintaining soft consistency on table constraints will be described.