Arrow Research search

Author name cluster

David G. Mitchell

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.

11 papers
2 author rows

Possible papers

11

LPAR Conference 2017 Conference Paper

Propagators and Solvers for the Algebra of Modular Systems

  • Bart Bogaerts 0001
  • Eugenia Ternovska
  • David G. Mitchell

Solving complex problems can involve non-trivial combinations of distinct knowledge bases and problem solvers. The Algebra of Modular Systems is a knowledge representation framework that provides a method for formally specifying such systems in purely semantic terms. Many practical systems based on expressive formalisms solve the model expansion task. In this paper, we con- struct a solver for the model expansion task for a complex modular system from an expression in the algebra and black-box propagators or solvers for the primitive modules. To this end, we define a general notion of propagators equipped with an explanation mechanism, an extension of the algebra to propagators, and a lazy conflict-driven learning algorithm. The result is a framework for seamlessly combining solving technology from different domains to produce a solver for a combined system.

Details

LPAR Conference 2012 Conference Paper

Enfragmo: A System for Modelling and Solving Search Problems with Logic

  • Amir Aavani
  • Xiongnan (Newman) Wu
  • Shahab Tasharrofi
  • Eugenia Ternovska
  • David G. Mitchell

Abstract In this paper, we present the Enfragmo system for specifying and solving combinatorial search problems. It supports natural specification of problems by providing users with a rich language, based on an extension of first order logic. Enfragmo takes as input a problem specification and a problem instance and produces a propositional CNF formula representing solutions to the instance, which is sent to a SAT solver. Because the specification language is high level, Enfragmo provides combinatorial problem solving capability to users without expertise in use of SAT solvers or algorithms for solving combinatorial problems. Here, we describe the specification language and implementation of Enfragmo, and give experimental evidence that its performance is comparable to that of related systems.

Details

IJCAI Conference 2009 Conference Paper

  • Eugenia Ternovska
  • David G. Mitchell

We address the problem of providing a logical formalization of arithmetic in declarative modelling languages for NP search problems. The challenge is to simultaneously allow quantification over an in- finite domain such as the natural numbers, provide natural modelling facilities, and control expressive power of the language. To address the problem, we introduce an extension of the model expansion (MX) based framework to finite structures embedded in an infinite secondary structure, together with “double-guarded” logics for representing MX specifications for these structures. The logics also contain multi-set functions (aggregate operations). Our main result is that these logics capture the complexity class NP on “small-cost” arithmetical structures.

PDF Details

LPAR Conference 2007 Conference Paper

Faster Phylogenetic Inference with MXG

  • David G. Mitchell
  • Faraz Hach
  • Raheleh Mohebali

Abstract We apply the logic-based declarative programming approach of Model Expansion (MX) to a phylogenetic inference task. We axiomatize the task in multi-sorted first-order logic with cardinality constraints. Using the model expansion solver MXG and SAT+cardinality solver MXC, we compare the performance of several MX axiomatizations on a challenging set of test instances. Our methods perform orders of magnitude faster than previously reported declarative solutions. Our best solution involves polynomial-time pre-processing, redundant axioms, and symmetry-breaking axioms. We also discuss our method of test instance generation, and the role of pre-processing in declarative programming.

Details

LPAR Conference 2006 Conference Paper

Constructing Camin-Sokal Phylogenies Via Answer Set Programming

  • Jonathan Kavanagh
  • David G. Mitchell
  • Eugenia Ternovska
  • Ján Manuch
  • Xiaohong Zhao
  • Arvind Gupta

Abstract Constructing parsimonious phylogenetic trees from species data is a central problem in phylogenetics, and has diverse applications, even outside biology. Many variations of the problem, including the cladistic Camin-Sokal (CCS) version, are NP-complete. We present Answer Set Programming (ASP) models for the binary CCS problem, as well as a simpler perfect phylogeny version, along with experimental results of applying the models to biological data. Our contribution is three-fold. First, we solve phylogeny problems which have not previously been tackled by ASP. Second, we report on variants of our CCS model which significantly affect run time, including the interesting case of making the program “slightly tighter”. This version exhibits some of the best performance, in contrast with a tight version of the model which exhibited poor performance. Third, we are able to find proven-optimal solutions for larger instances of the CCS problem than the widely used branch-and-bound-based PHYLIP package.

Details

SAT Conference 2006 Conference Paper

Minimum Witnesses for Unsatisfiable 2CNFs

  • Joshua Buresh-Oppenheim
  • David G. Mitchell

Abstract We consider the problem of finding the smallest proof of unsatisfiability of a 2CNF formula. In particular, we look at Resolution refutations and at minimum unsatisfiable subsets of the clauses of the CNF. We give a characterization of minimum tree-like Resolution refutations that explains why, to find them, it is not sufficient to find shortest paths in the implication graph of the CNF. The characterization allows us to develop an efficient algorithm for finding a smallest tree-like refutation and to show that the size of such a refutation is a good approximation to the size of the smallest general refutation. We also give a polynomial time dynamic programming algorithm for finding a smallest unsatisfiable subset of the clauses of a 2CNF.

Details

AAAI Conference 2005 Conference Paper

A Framework for Representing and Solving NP Search Problems

  • David G. Mitchell

NP search and decision problems occur widely in AI, and a number of general-purpose methods for solving them have been developed. The dominant approaches include propositional satisfiability (SAT), constraint satisfaction problems (CSP), and answer set programming (ASP). Here, we propose a declarative constraint programming framework which we believe combines many strengths of these approaches, while addressing weaknesses in each of them. We formalize our approach as a model extension problem, which is based on the classical notion of extension of a structure by new relations. A parameterized version of this problem captures NP. We discuss properties of the formal framework intended to support effective modelling, and prospects for effective solver design.

PDF Details

AAAI Conference 1998 Conference Paper

Hard Problems for CSP Algorithms

  • David G. Mitchell

Weprove exponential lower bounds on the running time of manyalgorithms for Constraint Satisfaction, by giving a simple family of instances on which they always take exponential time. Although similar lower bounds for most of these algorithms have been shown before, we provide a uniform treatment which illustrates a powerful general approach and has stronger impfications for the practice of algorithm design.

PDF Details