David Mitchell - Publications

David G. Mitchell - Selected Publications, Etc.

Satisfiability and Constraint Satisfaction

Simplifying CDCL Clause Database Reduction (preprint). with Sima Jamali. Proc. SAT 2019, Lisbon, July 2019.
Centrality Based Improvements to CDCL Solvers (preprint). with Sima Jamali. Proc. SAT 2018, Oxford UK, July 2018.
Improving SAT Solver Performance with Stucture-Based Preferential Bumping.(preprint) with Sima Jamali. Proc. 3rd Global Conference on Artificial Intelligence, Miama FL, October 2017.

Resolution and Clause Learning with Restarts for Signed CNF Formulas (local pre-print) IfCoLog Journal of Logics and Their Applications, Volume 4, Number 7, Pages 1905--1926

Propagators and Solvers for the Algebra of Modular Systems with Bart Bogaerts and Evgenia Ternovska. Proc. LPAR 2017.

Clause Learning for Modular Systems. With Eugenia Ternovska. In: Proc., LPNMR 2015

Minimum 2CNF Resolution Refutations in Polynomial Time. With Joshua Buresh-Oppenheim. In: Proc., SAT-2007

Minimum Witnesses for Unsatisfiable 2CNFs. With Joshua Buresh-Oppenheim. In: Proc., SAT-2006

A SAT Solver Primer. EATCS Bulletin (The Logic in Computer Science Column), Volume 85, February 2005, pages 112-133. (Citations and Uses as Course Readings - out of date)

2-way vs. d-way Branching for CSP. With Joey Hwang. In: Principles and Practices of Constraint Programming - CP 2005, Proceedings (Springer, LNCS-????).

The Resolution Complexity of Random Graph $k$-colorability. With Paul Beame, Joseph Culberson and Christopher Moore. Discrete Applied Mathematics Volume 153, Issues 1-3 , 1 December 2005, Pages 25-47. (Also ECCC Report TR04-012.)

Resolution and Constraint Satisfaction, David G. Mitchell. In: Principles and Practices of Constraint Programming - CP 2003, Proceedings (Springer, LNCS-2833).

Resolution Complexity of Random Constraints, In: Principles and Practices of Constraint Programming - CP 2002, Proceedings (Springer, LNCS-2470).

Hard Problems for CSP Algorithms, In: Proc., Fifteenth National Conf. on Artificial Intelligence, Madison WI, July 1998, AAAI Press/MIT Press.

Finding Hard Instances of the Satisfiability Problem: A Survey, With Stephen Cook. In: Satisfiability Problem: Theory and Applications, Du, Gu and Pardalos (Eds). DIMACS Series in Discrete Mathamatics and Theoretical Computer Science, Volume 35, 1997, pages 1-17.

Generating Hard Satisfiability Problems, With Bart Selman and Hector Levesque,
Artificial Intelligence, Volume 81(1-2), March 1996, pages 17-29.

Some Pitfalls for Experimenters with Random SAT, With Hector Levesque,
Artificial Intelligence, Volume 81(1-2), March 1996, pages 111-125.

A New Method for Solving Hard Satisfiability Problems, With Bart Selman and Hector Levesque. Proc., Tenth National Conf. on Artificial Intelligence ,San Jose, CA, July 1992, AAAI Press/MIT Press, pages 440-446.

Hard and Easy Distributions of SAT Problems, With Bart Selman and Hector Levesque,
Proc., Tenth National Conf. on Artificial Intelligence ,San Jose, CA, July 1992, AAAI Press/MIT Press, pages 459-465.

Declarative Solving: Representation Languages, Grounding and Reductions, etc.

On Correctness of Models and Reformulations (Preliminary Version) PTHG-20: The Fourth Workshop on Progress Towards the Holy Grail

Guarded Constraint Models Define Treewidth-Preserving Reductions. CP 2019

Instance Transformation fo Declarative Solvers. With Megan O'Connor. IEMCON 2015
Lifted Unit Propagation for Effective Grounding. With Pashootan Vaezipour and Maarten Marien. Proc., INAP 2011.

Speed-Up Techniques for Negation in Grounding. With Amir Aavani, Shahab Tasharrofi, Gulay Ünel and Eugenia Ternovska. LPAR (Dakar) 2010:13-26

Declarative Programming of Search Problems with Built-in Arithmetic. With Eugenia Ternovska. and David G. Mitchell. IJCAI 2009
Modelling Languages, Model Expansion, and MXG. Invited Talk, WOG Seminar on Logic and Computation, April 29, 2008.

Expressiveness and Abstraction in Essence. With Eugenia Ternovska. Constraints, Volume 13, Issue 3, pages 343-384.

An MX-based Front End for SAT. Invited talk, NSF Workshop on the status and future of SAT, March 2008.

Constraint Programming with Unrestricted Quantification. David G. Mitchell and Eugenia Ternovska, First International Workshop on Quantification in Constraint Programming (CP-2005 Workshop)

Model Expansion as a Framework for Modelling and Solving Search Problems. With Eugenia Ternovska, Faraz Hach and Raheleh Mohebali. SFU Computing Science Technical Report TR-2006-24. Bibtex Entry
A Framework for Representing and Solving NP Search Problems. With Eugenia Ternovska. In: Proc., Twentieth National Conf. on Artificial Intelligence (AAAI-05), Pittsburgh, PA, July 2005, AAAI Press/MIT Press, pages 430-435.

Systems, Applications, Software

Enfragmo: A System for Modelling and Solving Search Problems with Logic. With Amir Aavani, Xiongnan (Newman) Wu, Shahab Tasharrofi and Eugenia Ternovska. LPAR 2012:15-22.

The SAT Solver MXC, Version 0.5 With David Bregman. Solver Description for the 2007 SAT Solver Competition.

The SAT Solver MXC, Version 0.1 David R. Bregman and David G. Mitchell. Solver Description for SAT Race 2006 Solver Competition.

Faster Phylogenetic Inference with MXG. With Faraz Hach and Raheleh Mohebali. Proc. of LPAR-2007: LNCS 4790, pp 423--437 Bibtex

Constructing Cladistic Camin-Sokal Phylogeny Trees Via Answer Set Programming. With Jonathan Kavanagh, Eugenia Ternovska, Xiaohong Zhao, Jano Manuch and Arvind Gupta. Proc. of LPAR-2006, LNCS 4246, pp 452-466.

Theses

The Resolution Complexity of Constraint Satisfaction,
Ph.D. Thesis, University of Toronto, 2002.

An Empirical Study of Random SAT,
M.Sc. Thesis, Simon Fraser University, 1993.

Back to Dr. Mitchell's Home Page