David G. Mitchell - Selected Publication, Etc.

Satisfiability and Constraint Satisfaction

• Minimum 2CNF Resolution Refutations in Polynomial Time. Joshua Buresh-Oppenheim and David Mitchell. In: Proc., SAT-2007
• Minimum Witnesses for Unsatisfiable 2CNFs. Joshua Buresh-Oppenheim and David Mitchell. In: Proc., SAT-2006
• A SAT Solver Primer. David G. Mitchell, 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. Joey Hwang and David G. Mitchell. In: Principles and Practices of Constraint Programming - CP 2005, Proceedings (Springer, LNCS-????).
• 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, David G. Mitchell.
  In: Principles and Practices of Constraint Programming - CP 2002, Proceedings (Springer, LNCS-2470).
  
• Hard Problems for CSP Algorithms, David G. Mitchell.
  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, Stephen A. Cook and David G. Mitchell,
  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, Bart Selman, David G. Mitchell and Hector J. Levesque,
  Artificial Intelligence, Volume 81(1-2), March 1996, pages 17-29.
• Some Pitfalls for Experimenters with Random SAT, David G. Mitchell and Hector J. Levesque,
  Artificial Intelligence, Volume 81(1-2), March 1996, pages 111-125.
• A New Method for Solving Hard Satisfiability Problems, Bart Selman, Hector J. Levesque and David G. Mitchell,
  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, David G. Mitchell, Bart Selman and Hector J. Levesque,
  Proc., Tenth National Conf. on Artificial Intelligence ,San Jose, CA, July 1992, AAAI Press/MIT Press, pages 459-465.

Representation Languages for Declarative Problem Solving

• Declarative Programming of Search Problems with Built-in Arithmetic. 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. David G. Mitchell and 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.
• Model Expansion as a Framework for Modelling and Solving Search Problems. David Mitchell, Eugenia Ternovska, Faraz Hach, Raheleh Mohebali. SFU Computing Science Technical Report TR-2006-24. Bibtex Entry
• A Framework for Representing and Solving NP Search Problems. David G. Mitchell and Eugenia Ternovska, In: Proc., Twentieth National Conf. on Artificial Intelligence (AAAI-05), Pittsburgh, PA, July 2005, AAAI Press/MIT Press, pages 430-435.

• Solving NP Search Problems with Model Expansion. Faraz Hach, MSc. Thesis, 2007.
• A Method for Solving NP Search Based on Model Expansion and Grounding. Raheleh Mohebali, MSc. Thesis, 2007.
• Modelling with FO(ID), Solving with SAT. David Mitchell and Eugenia Ternovska. Talk from the Workshop on Constraints and Verification, at the Isaac Newton Institute, Cambridge, May 2006.
• The Resolution Complexity of Random Graph $k$-colorability. Paul Beame, Joseph Culberson, David Mitchell and Christopher Moore. Discrete Applied Mathematics Volume 153, Issues 1-3 , 1 December 2005, Pages 25-47. (Also ECCC Report TR04-012.)
• The SAT Solver MXC, Version 0.1 David R. Bregman and David G. Mitchell. Solver Description for SAT Race 2006 Solver Competition.
• Constraint Programming with Unrestricted Quantification. David G. Mitchell and Eugenia Ternovska, First International Workshop on Quantification in Constraint Programming (CP-2005 Workshop)
• A Theoretical Comparison of Resolution Systems for CSP Algorithms. Joey Hwang MSc. Thesis, 2004.
• Efficient Algorithms for Clause Learning SAT Solvers. Lawrence Ryan MSc. Thesis, 2004.

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.