A number of problems involve managing a set of optional clauses. For example, the soft clauses in a MAXSAT formula are optional—they can be falsified for a cost. Similarly, when computing a Minimum Correction Set for an unsatisfiable formula, all clauses are optional—some can be falsified in order to satisfy the remaining. In both of these cases the task is to find a subset of the optional clauses that achieves some criteria, and whose removal leaves a satisfiable formula. Relaxation search is a simple method of using a standard SAT solver to solve this task. Relaxation search is easy to implement, sometimes requiring only a simple modification of the variable selection heuristic in the SAT solver; it offers considerable flexibility and control over the order in which subsets of optional clauses are examined; and it automatically exploits clause learning to exchange information between the two phases of finding a suitable subset of optional clauses and checking if their removal yields satisfiability. We demonstrate how relaxation search can be used to solve MAXSAT and to compute Minimum Correction Sets. In both cases relaxation search is able to achieve state-of-the-art performance and solve some instances other solvers are not able to solve.

This paper outlines an online approach for algorithm configuration which uses the power of modern multicore system to evaluate multiple parameters configurations in parallel.

The NP-hard number-partitioning problem is to separate a multiset S of n positive integers into k subsets, such that the largest sum of the integers assigned to any subset is minimized. The classic application is scheduling a set of n jobs with different run times onto k identical machines such that the makespan, the time to complete the schedule, is minimized. We present a new algorithm, cached iterative weakening (CIW), for solving this problem optimally. It incorporates three ideas distinct from the previous state of the art: it explores the search space using iterative weakening instead of branch and bound; generates feasible subsets once and caches them instead of at each node of the search tree; and explores subsets in cardinality order instead of an arbitrary order. The previous state of the art is represented by three different algorithms depending on the values of n and k. We provide one algorithm which outperforms all previous algorithms for k >= 4. Our run times are up to two orders of magnitude faster.

Partial MaxSAT (PMS) is a generalization to SAT and MaxSAT. Many real world problems can be encoded into PMS in a more natural and compact way than SAT and MaxSAT. In this paper, we propose new ideas for local search for PMS, which mainly rely on the distinction between hard and soft clauses. We use these ideas to develop a local search PMS algorithm called {\it Dist}. Experimental results on PMS benchmarks from MaxSAT Evaluation 2013 show that {\it Dist} significantly outperforms state-of-the-art PMS algorithms, including both local search algorithms and complete ones, on random and crafted benchmarks. For the industrial benchmark, {\it Dist} dramatically outperforms previous local search algorithms and is comparable with complete algorithms.

Our objective is to boost the state-of-the-art performance in MaxSATsolving. To this end, we employ the instance-specific algorithmconfigurator ISAC, and improve it with the latest inportfolio technology. Experimental results on SAT show that thiscombination marks a significant step forward in our ability to tunealgorithms instance-specifically. We then apply the new methodology toa number of MaxSAT problem domains and show that the resulting solversconsistently outperform the best existing solvers on the respectiveproblem families. In fact, the solvers presented here were independentlyevaluated at the 2013 MaxSAT Evaluation where they won six of the elevencategories.

The Game Description Language GDL is the standard input language for general game-playing systems. While players can gain a lot of traction by an efficient inference algorithm for GDL, state-of-the-art reasoners suffer from a variant of a classical KR problem, the inferential frame problem. We present a method by which general game players can transform any given game description into a representation that solves this problem. Our experimental results demonstrate that with the help of automatically generated domain knowledge, a significant speedup can thus be obtained for the majority of the game descriptions from the AAAI competition.

Compared to conventional cars, electric vehicles still suffer from a considerably shorter cruising range. Combined with the sparsity of battery loading stations, the complete transition to E-mobility still seems a long way to go. In this paper, we consider the problem of placing as few loading stations as possible such that on any shortest path there are enough to guarantee sufficient energy supply. This means, that EV owners no longer have to plan their trips ahead incorporating loading station locations, and are no longer forced to accept long detours to reach their destinations. We show how to model this problem and introduce heuristics which provide close-to-optimal solutions even in large road networks.

Multi-label learning concerns learning multiple, overlapping, and correlated classes. In this paper, we adapt a recent structured prediction framework called HC-Search for multi-label prediction problems. One of the main advantages of this framework is that its training is sensitive to the loss function, unlike the other multi-label approaches that either assume a specific loss function or require a manual adaptation to each loss function. We empirically evaluate our instantiation of the HC-Search framework along with many existing multi-label learning algorithms on a variety of benchmarks by employing diverse task loss functions. Our results demonstrate that the performance of existing algorithms tends to be very similar in most cases, and that the HC-Search approach is comparable and often better than all the other algorithms across different loss functions.

Utilizing multiple queues in Greedy Best-First Search (GBFS) has been proven to be a very effective approach to satisficing planning. Successful techniques include extra queues based on Helpful Actions (or Preferred Operators), as well as using Multiple Heuristics. One weakness of all standard GBFS algorithms is their lack of exploration. All queues used in these methods work as priority queues sorted by heuristic values. Therefore, misleading heuristics, especially early in the search process, can cause the search to become ineffective. Type systems, as introduced for heuristic search by Lelis et al, are a development of ideas for exploration related to the classic stratified sampling approach. The current work introduces a search algorithm that utilizes type systems in a new way – for exploration within a GBFS multiqueue framework in satisficing planning. A careful case study shows the benefits of such exploration for overcoming deficiencies of the heuristic. The proposed new baseline algorithm Type-GBFS solves almost 200 more problems than baseline GBFS over all International Planning Competition problems. Type-LAMA, a new planner which integrates Type-GBFS into LAMA-2011, solves 36.8 more problems than LAMA-2011.

We have introduced a new model of hedonic coalition formation game, which we call Roles and Teams Hedonic Games (RTHG). In this model, agents view coalitions as compositions of available roles. An agent's utility for a partition is based upon which role she fulfills within the coalition and which roles are being fulfilled within the coalition. The major contributions of the paper include designing the RTHG model, with its corresponding stability and (NP-hard) optimization criteria, designing a heuristic partitioning algorithm and local search algorithm, implementation and testing.