We study decompositions of NVALUE, a global constraint that can be used to model a wide range of problems where values need to be counted. Whilst decomposition typically hinders propagation, we identify one decomposition that maintains a global view as enforcing bound consistency on the decomposition achieves bound consistency on the original global NVALUE constraint. Such decompositions offer the prospect for advanced solving techniques like nogood learning and impact based branching heuristics. They may also help SAT and IP solvers take advantage of the propagation of global constraints.

In the satisfiability domain, it is well-known that a SAT algorithm may solve a problem instance easily and another instance hardly, whilst these two instances are equivalent CNF encodings of the original problem. Moreover, different algorithms may disagree on which encoding makes the problem easier to solve. In this paper, we focus on the CNF encoding of cardinality constraints, which states that exactly k propositional variables in a given set are assigned to true. We demonstrate the importance of the semantics of the SAT variables in the encoding of this constraint. We implement several variants of the CNF encoding in which the close semantic variables are grouped. We then examine these new encodings on problems generated from diagnosis of discrete-event system. Our results demonstrate that both stochastic and systematic SAT algorithms can now solve most of the problem instances, which were unreachable before. These results also indicate that, on average cases, there is an encoding that suits well both SLS and DPLL algorithms.

Practically all programming languages allow the programmer to split a program into several modules which brings along several advantages in software development. In this paper, we are interested in the area of answer-set programming where fully declarative and nonmonotonic languages are applied. In this context, obtaining a modular structure for programs is by no means straightforward since the output of an entire program cannot in general be composed from the output of its components. To better understand the effects of disjunctive information on modularity we restrict the scope of analysis to the case of disjunctive logic programs (DLPs) subject to stable-model semantics. We define the notion of a DLP-function, where a well-defined input/output interface is provided, and establish a novel module theorem which indicates the compositionality of stable-model semantics for DLP-functions. The module theorem extends the well-known splitting-set theorem and enables the decomposition of DLP-functions given their strongly connected components based on positive dependencies induced by rules. In this setting, it is also possible to split shared disjunctive rules among components using a generalized shifting technique. The concept of modular equivalence is introduced for the mutual comparison of DLP-functions using a generalization of a translation-based verification method.

This paper presents a multilayered architecture that enhances the capabilities of current QA systems and allows different types of complex questions or queries to be processed. The answers to these questions need to be gathered from factual information scattered throughout different documents. Specifically, we designed a specialized layer to process the different types of temporal questions. Complex temporal questions are first decomposed into simple questions, according to the temporal relations expressed in the original question. In the same way, the answers to the resulting simple questions are recomposed, fulfilling the temporal restrictions of the original complex question. A novel aspect of this approach resides in the decomposition which uses a minimal quantity of resources, with the final aim of obtaining a portable platform that is easily extensible to other languages. In this paper we also present a methodology for evaluation of the decomposition of the questions as well as the ability of the implemented temporal layer to perform at a multilingual level. The temporal layer was first performed for English, then evaluated and compared with: a) a general purpose QA system (F-measure 65.47% for QA plus English temporal layer vs. 38.01% for the general QA system), and b) a well-known QA system. Much better results were obtained for temporal questions with the multilayered system. This system was therefore extended to Spanish and very good results were again obtained in the evaluation (F-measure 40.36% for QA plus Spanish temporal layer vs. 22.94% for the general QA system).

In this paper, we investigate knowledge reasoning within a simple framework called knowledge structure. We use variable forgetting as a basic operation for one agent to reason about its own or other agents\' knowledge. In our framework, two notions namely agents\' observable variables and the weakest sufficient condition play important roles in knowledge reasoning. Given a background knowledge base and a set of observable variables for each agent, we show that the notion of an agent knowing a formula can be defined as a weakest sufficient condition of the formula under background knowledge base. Moreover, we show how to capture the notion of common knowledge by using a generalized notion of weakest sufficient condition. Also, we show that public announcement operator can be conveniently dealt with via our notion of knowledge structure. Further, we explore the computational complexity of the problem whether an epistemic formula is realized in a knowledge structure. In the general case, this problem is PSPACE-hard; however, for some interesting subcases, it can be reduced to co-NP. Finally, we discuss possible applications of our framework in some interesting domains such as the automated analysis of the well-known muddy children puzzle and the verification of the revised Needham-Schroeder protocol. We believe that there are many scenarios where the natural presentation of the available information about knowledge is under the form of a knowledge structure. What makes it valuable compared with the corresponding multi-agent S5 Kripke structure is that it can be much more succinct.

We present two different methods for estimating the cost of solving SAT problems. The methods focus on the online behaviour of the backtracking solver, as well as the structure of the problem. Modern SAT solvers present several challenges to estimate search cost including coping with nonchronological backtracking, learning and restarts. Our first method adapt an existing algorithm for estimating the size of a search tree to deal with these challenges. We then suggest a second method that uses a linear model trained on data gathered online at the start of search. We compare the effectiveness of these two methods using random and structured problems. We also demonstrate that predictions made in early restarts can be used to improve later predictions. We conclude by showing that the cost of solving a set of problems can be reduced by selecting a solver from a portfolio based on such cost estimations.

Restart strategies are an important factor in the performance of conflict-driven Davis Putnam style SAT solvers. Selecting a good restart strategy for a problem instance can enhance the performance of a solver. Inspired by recent success applying machine learning techniques to predict the runtime of SAT solvers, we present a method which uses machine learning to boost solver performance through a smart selection of the restart strategy. Based on easy to compute features, we train both a satisfiability classifier and runtime models. We use these models to choose between restart strategies. We present experimental results comparing this technique with the most commonly used restart strategies. Our results demonstrate that machine learning is effective in improving solver performance.

Capability planning problems are pervasive throughout many areas of human interest with prominent examples found in defense and security. Planning provides a unique context for optimization that has not been explored in great detail and involves a number of interesting challenges which are distinct from traditional optimization research. Planning problems demand solutions that can satisfy a number of competing objectives on multiple scales related to robustness, adaptiveness, risk, etc. The scenario method is a key approach for planning. Scenarios can be defined for long-term as well as short-term plans. This paper introduces computational scenario-based planning problems and proposes ways to accommodate strategic positioning within the tactical planning domain. We demonstrate the methodology in a resource planning problem that is solved with a multi-objective evolutionary algorithm. Our discussion and results highlight the fact that scenario-based planning is naturally framed within a multi-objective setting. However, the conflicting objectives occur on different system levels rather than within a single system alone. This paper also contends that planning problems are of vital interest in many human endeavors and that Evolutionary Computation may be well positioned for this problem domain.

Scenarios are pen-pictures of plausible futures, used for strategic planning. The aim of this investigation is to expand the horizon of scenario-based planning through computational models that are able to aid the analyst in the planning process. The investigation builds upon the advances of Information and Communication Technology (ICT) to create a novel, flexible and customizable computational capability-based planning methodology that is practical and theoretically sound. We will show how evolutionary computation, in particular evolutionary multi-objective optimization, can play a central role - both as an optimizer and as a source for innovation.

This paper demonstrates that simple yet important characteristics of coevolution can occur in evolutionary algorithms when only a few conditions are met. We find that interaction-based fitness measurements such as fitness (linear) ranking allow for a form of coevolutionary dynamics that is observed when 1) changes are made in what solutions are able to interact during the ranking process and 2) evolution takes place in a multi-objective environment. This research contributes to the study of simulated evolution in a at least two ways. First, it establishes a broader relationship between coevolution and multi-objective optimization than has been previously considered in the literature. Second, it demonstrates that the preconditions for coevolutionary behavior are weaker than previously thought. In particular, our model indicates that direct cooperation or competition between species is not required for coevolution to take place. Moreover, our experiments provide evidence that environmental perturbations can drive coevolutionary processes; a conclusion that mirrors arguments put forth in dual phase evolution theory. In the discussion, we briefly consider how our results may shed light onto this and other recent theories of evolution.