We investigate the  complexity of  satisfiability for one-agent refinement modal logic (RML), an extension of basic modal logic (ML) obtained by adding refinement quantifiers on structures.  RML is known to have the same expressiveness as ML, but the translation of RML into ML is of non-elementary complexity, and RML is at least doubly exponentially more succinct than ML. In this paper we show that RML-satisfiability is `only' singly exponentially harder than ML-satisfiability, the latter being a well-known PSPACE-complete problem.

We establish the unexpected power of conflict driven clause learning (CDCL) proof search by proving that the sets of unsatisfiable clauses obtained from the guarded graph tautology principles of Alekhnovich, Johannsen, Pitassi and Urquhart have polynomial size pool resolution refutations that use only input lemmas as learned clauses. We further show that, under the correct heuristic choices, these refutations can be carried out in polynomial time by CDCL proof search without restarts, even when restricted to greedy, unit-propagating search. The guarded graph tautologies had been conjectured to separate CDCL without restarts from resolution; our results refute this conjecture.

Social norms are one of the mechanisms for decentralized societies to achieve coordination amongst individuals. Such norms are conflict resolution strategies that develop from the population interactions instead of a centralized entity dictating agent protocol.One of the most important characteristics of social norms is that they are imposed by the members of the society, and they are responsible for the fulfillment and defense of these norms. By allowing agents to manage (impose, abide by and defend) social norms, societies achieve a higher degree of freedom by lacking the necessity of authorities supervising all the interactions amongst agents. In this article we summarize the contributions of my dissertation, where we provide an unifying framework for the analysis of social norms in virtual societies, providing an strong emphasis on virtual agents and humans.

Mobile manipulation robots are envisioned to provide many useful services both in domestic environments as well as in the industrial context.  In this paper, we present novel approaches to allow mobile maniplation systems to autonomously adapt to new or changing situations. The approaches developed in this paper cover the following four topics: (1) learning the robot's kinematic structure and properties using actuation and visual feedback, (2) learning about articulated objects in the environment in which the robot is operating, (3) using tactile feedback to augment visual perception, and (4) learning novel manipulation tasks from human demonstrations.

Automated planning is the process of automatically selecting actions that achieve a desired outcome. This paper summarises several contributions that improve the efficiency of automated planning via heuristic search. We discuss novel heuristics based on landmarks and a search algorithm for anytime planning. Furthermore, we analyse various search-enhancement techniques and show how the combination of these techniques lead to a planning system that proved highly successful in the 2008 and 2011 International Planning Competitions.

In human conversation, meaning is transported through several channels such as verbal and nonverbal behavior. Certain of these behavioral aspects are culturally dependent. Mutual understanding or acceptance is thus, amongst others, depended on the cultural background of the interlocutors. When designing virtual character behavior, culture should be considered as it may improve the character's acceptance by users of certain cultural backgrounds. This paper proposes a hybrid approach for the generation of culture-specific behaviors in a multiagent system. A computational model has been established by refining theoretical knowledge of culture-specific behavior with statistical data extracted from a video corpus of German and Japanese first-time meetings. Evaluation studies of such culturally enhanced virtual characters were conducted in both targeted cultures. Results indicate that human observers tend to prefer character behavior that was designed to resemble their own cultural background.

Combinatorial Optimization is an important area of computer science that has many theoretical and practical applications. In the thesis, we present important contributions to several different areas of combinatorial optimization, including nogood learning, symmetry breaking, dominance, relaxations and parallelization. We develop a new nogood learning technique based on constraint projection that allows us to exploit subproblem dominances that arise when two different search paths lead to subproblems which are identical on the remaining unfixed variables. We present a new symmetry breaking technique called SBDS-1UIP, which extends Symmetry Breaking During Search (SBDS) by using the more powerful 1UIP nogoods generated by Lazy Clause Generation (LCG) solvers. We present two new general methods for exploiting almost symmetries by modifying SBDS-1UIP and by using conditional symmetry breaking constraints. We solve the Minimization of Open Stacks Problem, the Talent Scheduling Problem (CSPLib prob039), and the Maximum Density Still Life Problem (CSPLib prob032) many orders of magnitude faster than the previous state of the art by applying various powerful techniques such as nogood learning, dynamic programming, dominance and relaxations. We present cache aware data structures for SAT solvers which allows sequential and parallel versions of SAT solvers to run more quickly. And we present a new load balancing scheme for parallel search called confidence based work stealing, which allows the parallel search to make use of the information contained in the branching heuristic.

Online content have become an important medium to disseminate information and express opinions. With their proliferation, users are faced with the problem of missing the big picture in a sea of irrelevant and/or diverse content. In this paper, we addresses the problem of information organization of online document collections, and provide algorithms that create a structured representation of the otherwise unstructured content. We leverage the expressiveness of latent probabilistic models (e.g., topic models) and non-parametric Bayes techniques (e.g., Dirichlet processes), and give online and distributed inference algorithms that scale to terabyte datasets and adapt the inferred representation with the arrival of new documents. This paper is an extended abstract of the 2012 ACM SIGKDD best doctoral dissertation award of Ahmed [2011].

Qualitative models are predictive models that describe how changes in values of input variables affect the output variable in qualitative terms, e.g. increasing or decreasing. We describe Padé, a new method for qualitative learning which estimates partial derivatives of the target function from training data and uses them to induce qualitative models of the target function. We formulated three methods for computation of derivatives, all based on using linear regression on local neighbourhoods. The methods were empirically tested on artificial and real-world data. We also provide a case study which shows how the developed methods can be used in practice.

Evolutionary algorithms (EAs) are a large family of heuristic optimization algorithms inspired by natural phenomena, and are often used in practice to obtain satisficing instead of optimal solutions. In this work, we investigate a largely underexplored issue: the approximation performance of EAs in terms of how close the obtained solution is to an optimal solution. We study an EA framework named simple EA with isolated population (SEIP) that can be implemented as a single- or multi-objective EA. We present general approximation results of SEIP, and specifically on the minimum set cover problem, we find that SEIP achieves the currently best-achievable approximation ratio. Moreover, on an instance class of the k -set cover problem, we disclose how SEIP can overcome the difficulty that limits the greedy algorithm.