But this premature paving is not very useful if the searchtree is explored depth-first (DFS) or breadth-first (BFS): DFS When applied to numerical CSPs, the branch and quickly converges to ɛ-boxes that are too close to one another prune algorithm (BPA) computes a sharp covering to be representative of the solution set (see the left part of of the solution set. The BPA is therefore impractical Figure 1); BFS computes a homogeneous paving but finds no when the solution set is large, typically when ɛ-box at all if stopped too early (see the center graphic of Figure it has a dimension larger than four or five which is 1; note that such a sharp paving cannot be computed for often met in underconstrained problems. The purpose larger solution sets, making BFS useless in such cases). of this paper is to present a new search tree The search strategy used in an anytime BPA should quickly exploration strategy for BPA that hybridizes depthfirst find ɛ-boxes that are representative of the solution set: ɛ- and breadth-first searches. This search strategy boxes should be discovered uniformly on a continuous connected allows the BPA discovering potential solutions component in the solution set, while every connected in different areas of the search space in early stages components should be reached by some ɛ-boxes in early of the exploration, hence allowing an anytime usage stages of the search. Two such strategies are introduced in of the BPA. The merits of the proposed search the present paper. The most distant-first strategy (MDFS) strategy are experimentally evaluated.

In Model-Based Diagnosis (MBD), the problem of computing a diagnosis in a strong-fault model (SFM) is computationally much harder than in a weak-fault model (WFM). For example, in propositional Horn models, computing the first minimal diagnosis in a weak-fault model (WFM) is in P but is NP-hard for strong-fault models. As a result, SFM problems of practical significance have not been studied in great depth within the MBD community. In this paper we describe an algorithm that renders the problem of computing a diagnosis in several important SFM subclasses no harder than a similar computation in a WFM. We propose an approach for efficiently computing minimal diagnoses for these subclasses of SFM that extends existing conflict-based algorithms like GDE (Sherlock) and CDA*. Experiments on ISCAS85 combinational circuits show (1) inference speedups with CDA* of up to a factor of 8, and (2) an average of 28% reduction in the average conflict size, at the price of an extra low-polynomial-time consistency check for a candidate diagnosis.

We consider the problem of planning in domains with continuous linear numeric change. Such change cannot always be adequately modelled by discretisation and is a key facet of many interesting problems. We show how a forward-chaining temporal planner can be extended to reason with actions with continuous linear effects. We extend a temporal planner to handle numeric values using linear programming. We show how linear continuous change can be integrated into the same linear program and we discuss how a temporal-numeric heuristic can be used to provide the search guidance necessary to underpin continuous planning. We present results to show that the approach can effectively handle duration-dependent change and numeric variables subject to continuous linear change.

We present and analyze coalitional affinity games, a family of hedonic games that explicitly model the value that an agent receives from being associated with other agents.  We provide a characterization of the social-welfare maximizing coalition structures, and study the stability properties of affinity games, using the core solution concept.  Interestingly, we observe that members of the core do not necessarily maximize social welfare.  We introduce a new measure, the stability-gap to capture this difference.  Using the stability gap, we show that for an interesting class of coalitional affinity games, the difference between the social welfare of a stable coalition structure and a social welfare maximizing coalition structure is bounded by a factor of two, and that this bound is tight.

The Possible Winner problem asks whether some distinguished candidate may  become the winner of an election when the given incomplete votes are extended into complete ones in a favorable way. Possible Winner is NP-complete for common voting rules such as Borda, many other positional scoring rules, Bucklin, Copeland etc.  We investigate how three different parameterizations influence the computational complexity of Possible Winner for a number of voting rules.  We show  fixed-parameter tractability results with respect to the parameter "number of candidates" but intractability results with respect to the parameter "number of votes". Finally, we derive fixed-parameter tractability results with respect to the parameter "total number of undetermined candidate pairs" and identify an interesting polynomial-time solvable special case for Borda.

This paper deals with  multiobjective optimization in the context of multiattribute utility theory. The alternatives (feasible solutions) are seen as elements of a product set of attributes and preferences over solutions are represented by generalized additive decomposable (GAI) utility functions modeling individual preferences or criteria. Due to decomposability, utility vectors attached to solutions can be compiled into a graphical structure closely related to junction trees, the so-called GAI net. We first show how the structure of the GAI net can be used to determine efficiently the exact set of Pareto-optimal solutions in a product set and provide numerical tests on random instances. Since the exact determination of the Pareto set is intractable in worst case, we propose a near admissible algorithm with performance guarantee, exploiting the GAI structure to approximate the set of Pareto optimal solutions. We present numerical experimentations, showing that both utility decomposition and approximation significantly improve resolution times in multiobjective search problems.

In this paper we approach the problem of reasoning with quantified Boolean formulas (QBFs) by combining search and resolution, and by switching between them according to structural properties of QBFs. We provide empirical evidence that QBFs which cannot be solved by search or resolution alone, can be solved by combining them, and that our approach makes a proof-of-concept implementation competitive with current QBF solvers.

Recently, Argumentation Mechanism Design (ArgMD) was introduced as a new paradigm for studying argumentation among self-interested agents using game-theoretic techniques. Preliminary results showed a condition under which a direct mechanism based on Dung's grounded semantics is strategy-proof (i.e. truth enforcing). But these early results dealt with a highly restricted form of agent preferences, and assumed agents can only hide, but not lie about, arguments. In this paper, we characterise strategy-proofness under grounded semantics for a more realistic preference class (namely, focal arguments). We also provide the first analysis of the case where agents can lie.

Conflict driven clause learning, one of the most important component of modern SAT solvers, is also recognized as very important in parallel SAT solving. Indeed, it allows clause sharing between multiple processing units working on related (sub-)problems. However, without limitation, sharing clauses might lead to an exponential blow up in communication or to the sharing of irrelevant clauses. This paper, proposes two innovative policies to dynamically adjust the size of shared clauses between any pair of processing units. The first approach controls the overall number of exchanged clauses whereas the second additionally exploits the relevance quality of shared clauses. Experimental results show important improvements of the state-of the-art parallel SAT solver.

CAPTCHA has been widely deployed by commercial web sites as a security technology for purposes such as anti-spam. A common approach to evaluating the robustness of CAPTCHA is the use of machine learning techniques. Critical to this approach is the acquisition of an adequate set of labeled samples, on which the learning techniques are trained. However, such a sample labeling task is difficult for computers, since the strength of CAPTCHAs stems exactly from the difficulty computers have in recognizing either distorted texts or image contents. Therefore, until now, researchers have to manually label their samples, which is tedious and expensive. In this paper, we present Magic Bullet, a computer game that for the first time turns such sample labeling into a fun experience, and that achieves a labeling accuracy of as high as 98% for free. The game leverages human computation to address a task that cannot be easily automated, and it effectively streamlines the evaluation of CAPTCHAs. The game can also be used for other constructive purposes such as 1) developing better machine learning algorithms for handwriting recognition, and 2) training people’s typing skills.