Author name cluster

Jessica Davies

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

7 papers

1 author row

AAAI Conference 2016 Conference Paper

A Symbolic SAT-Based Algorithm for Almost-Sure Reachability with Small Strategies in POMDPs

Krishnendu Chatterjee
Martin Chmelík
Jessica Davies

POMDPs are standard models for probabilistic planning problems, where an agent interacts with an uncertain environment. We study the problem of almost-sure reachability, where given a set of target states, the question is to decide whether there is a policy to ensure that the target set is reached with probability 1 (almost-surely). While in general the problem is EXPTIMEcomplete, in many practical cases policies with a small amount of memory sufﬁce. Moreover, the existing solution to the problem is explicit, which ﬁrst requires to construct explicitly an exponential reduction to a belief-support MDP. In this work, we ﬁrst study the existence of observation-stationary strategies, which is NP-complete, and then small-memory strategies. We present a symbolic algorithm by an efﬁcient encoding to SAT and using a SAT solver for the problem. We report experimental results demonstrating the scalability of our symbolic (SAT-based) approach.

PDF Details

AIJ Journal 2014 Journal Article

Complexity of and algorithms for the manipulation of Borda, Nanson's and Baldwin's voting rules

Jessica Davies
George Katsirelos
Nina Narodytska
Toby Walsh
Lirong Xia

We investigate manipulation of the Borda voting rule, as well as two elimination style voting rules, Nanson's and Baldwin's voting rules, which are based on Borda voting. We argue that these rules have a number of desirable computational properties. For unweighted Borda voting, we prove that it is NP-hard for a coalition of two manipulators to compute a manipulation. This resolves a long-standing open problem in the computational complexity of manipulating common voting rules. We prove that manipulation of Baldwin's and Nanson's rules is computationally more difficult than manipulation of Borda, as it is NP-hard for a single manipulator to compute a manipulation. In addition, for Baldwin's and Nanson's rules with weighted votes, we prove that it is NP-hard for a coalition of manipulators to compute a manipulation with a small number of candidates. Because of these NP-hardness results, we compute manipulations using heuristic algorithms that attempt to minimise the number of manipulators. We propose several new heuristic methods. Experiments show that these methods significantly outperform the previously best known heuristic method for the Borda rule. Our results suggest that, whilst computing a manipulation of the Borda rule is NP-hard, computational complexity may provide only a weak barrier against manipulation in practice. In contrast to the Borda rule, our experiments with Baldwin's and Nanson's rules demonstrate that both of them are often more difficult to manipulate in practice. These results suggest that elimination style voting rules deserve further study.

Details DOI

AIJ Journal 2014 Journal Article

Computational protein design as an optimization problem

David Allouche
Isabelle André
Sophie Barbe
Jessica Davies
Simon de Givry
George Katsirelos
Barry O'Sullivan
Steve Prestwich

Proteins are chains of simple molecules called amino acids. The three-dimensional shape of a protein and its amino acid composition define its biological function. Over millions of years, living organisms have evolved a large catalog of proteins. By exploring the space of possible amino acid sequences, protein engineering aims at similarly designing tailored proteins with specific desirable properties. In Computational Protein Design (CPD), the challenge of identifying a protein that performs a given task is defined as the combinatorial optimization of a complex energy function over amino acid sequences. In this paper, we introduce the CPD problem and some of the main approaches that have been used by structural biologists to solve it, with an emphasis on the exact method embodied in the dead-end elimination / A ⁎ algorithm ( DEE / A ⁎ ). The CPD problem is a specific form of binary Cost Function Network (CFN, aka Weighted CSP). We show how DEE algorithms can be incorporated and suitably modified to be maintained during search, at reasonable computational cost. We then evaluate the efficiency of CFN algorithms as implemented in our solver toulbar2, on a set of real CPD instances built in collaboration with structural biologists. The CPD problem can be easily reduced to 0/1 Linear Programming, 0/1 Quadratic Programming, 0/1 Quadratic Optimization, Weighted Partial MaxSAT and Graphical Model optimization problems. We compare toulbar2 with these different approaches using a variety of solvers. We observe tremendous differences in the difficulty that each approach has on these instances. Overall, the CFN approach shows the best efficiency on these problems, improving by several orders of magnitude against the exact DEE / A ⁎ approach. The introduction of dead-end elimination before or during search allows to further improve these results.

Details DOI

AAAI Conference 2014 Conference Paper

Relaxation Search: A Simple Way of Managing Optional Clauses

Fahiem Bacchus
Jessica Davies
Maria Tsimpoukelli
George Katsirelos

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.

PDF Details

AAAI Conference 2012 Conference Paper

Eliminating the Weakest Link: Making Manipulation Intractable?

Jessica Davies
Nina Narodytska
Toby Walsh

Successive elimination of candidates is often a route to making manipulation intractable to compute. We prove that eliminating candidates does not necessarily increase the computational complexity of manipulation. However, for many voting rules used in practice, the computational complexity increases. For example, it is already known that it is NP-hard to compute how a single voter can manipulate the result of single transferable voting(the elimination version of plurality voting). We show here that it is NP-hard to compute how a single voter can manipulate the result of the elimination version of veto voting, of the closely related Coombs’ rule, and of the elimination versions of a general class of scoring rules.

PDF Details

AAAI Conference 2011 Conference Paper

Complexity of and Algorithms for Borda Manipulation

Jessica Davies
George Katsirelos
Nina Narodytska
Toby Walsh

We prove that it is NP-hard for a coalition of two manipulators to compute how to manipulate the Borda voting rule. This resolves one of the last open problems in the computational complexity of manipulating common voting rules. Because of this NP-hardness, we treat computing a manipulation as an approximation problem where we try to minimize the number of manipulators. Based on ideas from bin packing and multiprocessor scheduling, we propose two new approximation methods to compute manipulations of the Borda rule. Experiments show that these methods signiﬁcantly outperform the previous best known approximation method. We are able to ﬁnd optimal manipulations in almost all the randomly generated elections tested. Our results suggest that, whilst computing a manipulation of the Borda rule by a coalition is NP-hard, computational complexity may provide only a weak barrier against manipulation in practice.

PDF Details

AAAI Conference 2007 Conference Paper

Using More Reasoning to Improve #SAT Solving

Jessica Davies

Many real-world problems, including inference in Bayes Nets, can be reduced to #SAT, the problem of counting the number of models of a propositional theory. This has motivated the need for efﬁcient #SAT solvers. Currently, such solvers utilize a modiﬁed version of DPLL that employs decomposition and caching, techniques that signiﬁcantly increase the time it takes to process each node in the search space. In addition, the search space is signiﬁcantly larger than when solving SAT since we must continue searching even after the ﬁrst solution has been found. It has previously been demonstrated that the size of a DPLL search tree can be signiﬁcantly reduced by doing more reasoning at each node. However, for SAT the reductions gained are often not worth the extra time required. In this paper we verify the hypothesis that for #SAT this balance changes. In particular, we show that additional reasoning can reduce the size of a #SAT solver’s search space, that this reduction cannot always be achieved by the already utilized technique of clause learning, and that this additional reasoning can be cost effective.

PDF Details