IMG_0302.JPGJessica Davies                                                                            

 

I obtained a PhD in Computer Science in May, 2013, at the Department of Computer Science, University of Toronto, Canada. My advisor was Fahiem Bacchus. 

 

 

Research

 

My thesis is about exact algorithms for the Maximum Satisfiability problem (MAXSAT). I have also worked in the areas of SAT solving, model counting and probabilistic inference, Quantified Boolean Formulas, and the coalitional manipulation of voting rules in the area of computational social choice.

 

 

 

Software

 

·         Prequel is a preprocessor for Quantified Boolean Formulas (QBF) [Samulowtiz, Davies and Bacchus, CP-2006].

·         #2clseq is solver for the weighted model counting problem [Davies and Bacchus, AAAI-2007]. Please contact me to request a copy of the source code.

·         A no-name branch and bound MAXSAT solver, with bounding based on clause learning [Davies, Cho and Bacchus, CP-2010]. Please contact me to request a copy of the source code.

·         MaxHS is a MAXSAT solver that decomposes the problem into SAT and MILP [Davies and Bacchus, CP-2013]. Please contact me to request a copy of the source code.

 

Conference papers

 

1.      Jessica Davies and Fahiem Bacchus. Postponing Optimization to Speed Up MAXSAT Solving. To appear in the Proceedings of the 19th International Conference on Principles and Practice of Constraint Programming (CP 2013), 2013.

2.      Jessica Davies and Fahiem Bacchus. Exploiting the Power of MIP Solvers in MAXSAT. Proceedings of the 16th International Conference on Theory and Applications of Satisfiability Testing (SAT 2013), 2013.

3.      Jessica Davies, Nina Narodytska, and Toby Walsh. Eliminating the Weakest Link: Making Manipulation Intractable? Proceedings of the 26th Annual Conference on Artificial Intelligence (AAAI 2012), 2012.

4.      Jessica Davies, George Katsirelos, Nina Narodystka, and Toby Walsh. Complexity of and Algorithms for Borda Manipulation. Outstanding paper award. Proceedings of the 25th Annual Conference on Artificial Intelligence (AAAI 2011), 2011.

5.      Jessica Davies and Fahiem Bacchus. Solving MAXSAT by Solving a Sequence of Simpler SAT Instances. Proceedings of the 17th International Conference on Principles and Practice of Constraint Programming (CP 2011), 2011.

6.      Jessica Davies, Jeremy Cho, and Fahiem Bacchus. Using Learnt Clauses in MAXSAT. Proceedings of the 16th International Conference on Principles and Practice of Constraint Programming (CP 2010), 2010.

7.      Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel and Marsha Chechik. Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC.  Proceedings of the 7th Conference on Formal Methods of Computer Aided Design (FMCAD 2007), 2007.

8.      Jessica Davies and Fahiem Bacchus. Using More Reasoning to Improve #SAT Solving.  Proceedings of the 22nd Conference on Artificial Intelligence (AAAI 2007), 2007.

9.      Horst Samulowitz, Jessica Davies and Fahiem Bacchus. Preprocessing QBF. Proceedings of the 12th International Conference on Principles and Practice of Constraint Programming (CP 2006), 2006.

 

Journal papers

 

1.      Jessica Davies, George Katsirelos, Nina Narodystka, Toby Walsh, and Lirong Xia. Complexity of and Algorithms for the Manipulation of Borda, Nanson and Baldwin’s Voting Rules. Artificial Intelligence. Accepted, 2011.

2.      Jocelyn Simmonds, Jessica Davies, Arie Gurfinkel, and Marsha Chechik. Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC. International Journal on Software Tools for Technology Transfer (STTT). 12(5), p.319-335, 2010.

 

Workshop papers

 

1.      Jessica Davies, George Katsirelos, Nina Narodystka, and Toby Walsh. An Empirical Study of Borda Manipulation. Third International Workshop on Computational Social Choice (ComSoc 2010). Dusseldorf, Germany, 2010. Uniform Election Results. Urn Election Results. Uniform Votes. Urn Votes.

2.      Jessica Davies and Fahiem Bacchus.  Distributional Distributional Importance Sampling for Approximate Weighted Model Counting. The First Workshop on Counting Problems in CSP and SAT, and Other Neighbouring Problems (Counting '08). Sydney, Australia, 2008.

 

Curriculum Vitae