Jessica Davies
I am
a PhD candidate in the Department of
Computer Science at The University of Toronto,
Canada. My advisor is Fahiem Bacchus.
Research
I
work on 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. I am interested in
extending my work on MAXSAT to non-Boolean settings and combining my ideas with
algorithms from Constraint Programming and Mixed Integer Linear Programming.
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-2011]. MaxHS-eval13 is the version of MaxHS submitted to the 2013 Maxsat Evaluation. The default command line options will give the configuration used in the Evaluation. Please contact me to request a copy of the source code, or previous versions of the solver.
Conference
papers
1. 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.
2. 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.
3. 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.
4. 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.
5. 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.
6. Jessica
Davies and Fahiem Bacchus. Using More Reasoning
to Improve #SAT Solving. Proceedings
of the 22nd Conference on Artificial Intelligence (AAAI 2007), 2007.
7. 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.