Selected papers on constraint satisfactionJohn Slaney
This is the abstract of the paper: John Slaney. The duality between conflicts and diagnoses in the field of diagnosis, or between plans and landmarks in the field of plan- ning, or between unsatisfiable cores and minimal co-satisfiable sets in SAT or CSP solving, has been known for many years. Recent work in these communities (Davies and Bacchus, CP 2011, Bonet and Helmert, ECAI 2010, Haslum et al., ICAPS 2012, Stern et al. , AAAI 2012) has brought it to the fore as a topic of current inter- est. The present paper lays out the set-theoretic basis of the concept, and introduces a generic implementation of an algorithm based on it. This algorithm provides a method for converting decision pro- cedures into optimisation ones across a wide range of applications without the need to rewrite the decision procedure implementations. Initial experimental validation shows good performance on a number of benchmark problems from AI planning.
This is the abstract of the paper: Andreas Bauer, Viorica Botea, Mark Brown, Matt Gray, Daniel Harabor and John Slaney. We present G12IDE, a front-end for the G12 platform aimed at helping users create and work with constraint models in a manner independent from any underlying solver. G12IDE contains tools for writing and evaluating models using Zinc and provides a feature rich debugger for monitoring a running search process. Debugging a search, as opposed to debugging sequential code, requires concepts such as breakpoints and queries to be applied at a higher level than in standard debuggers. Our solution is to let users define special events which, once reached in a search, cause the debugger to halt and give back, possibly in a visual manner, useful information on the current state of the search. G12IDE also includes a number of visualisation tools for drawing graphs and trees, and additionally allows users to create arbitrary domain-specific visualisations, such as the drawing of a sequential plan when the constraint problem is in fact a planning problem. The inclusion of such powerful and flexible visualisation toolkit and its tight integration with the available debugging facilities is, to the best of our knowledge, completely novel.
This is from the Introduction to the paper: Anbulagan, Duc Nghia Pham, John Slaney and Abdul Sattar. Although powerful and complex preprocessors are important to the success of many systematic SAT solvers, to date there has been no systematic evaluation of of the effects of these preprocessors on SAT solvers, especially on local search techniques. In the present study, we attempt to address this lack using problems known to be hard for SLS.
This is the abstract of the paper: Anbulagan and John Slaney. We present a new and more efficient heuristic by restricting lookahead saturation (LAS) with NVO (neighbourhood variable ordering) and DEW (dynamic equality weighting). We report on the integration of this heuristic in Satz, a high-performance SAT solver, showing empirically that it significantly improves the performance on an extensive range of benchmark problems that exhibit hard structure.
This is the abstract of the paper: Anbulagan, Duc Nghia Pham, John Slaney and Abdul Sattar. Recent work on Stochastic Local Search (SLS) for the SAT and CSP domains has shown the importance of a dynamic (non-markovian) strategy for weighting clauses in order to escape from local minima. In this paper, we improve the performance of two best contemprorary clause weighting solvers, PAWS and SAPS, by integrating a propositional resolution procedure. We also extend the work to AdaptNovelty+, the best non-weighting SLS solver in the GSAT/WalkSAT series. One outcome is that our systems can solve some highly structured problems such as quasigroup existence and parity learning problems which were previously thought unsuitable for local search and which are completely out of reach of traditional solvers such as GSAT. Here we present empirical results showing that for a range of random and realworld benchmark problems, resolution-enhanced SLS solvers clearly outperform the alternatives.
Automated Reasoning and Exhaustive Search This is the introduction to the paper: J Slaney, M Fujita and M Stickel. This is a report of research carried out during 1992 and 1993 in which three different automated reasoning programs, DDPP, FINDER and MGTP were applied to a series of exhaustive search problems in the theory of quasigroups. All three of the programs succeeded in solving previously open problems concerning the existence of quasigroups satisfying certain additional conditions. Using different programs has allowed us to cross-check the results, helping reliability. We find this research interesting from several points of view: firstly in that it brings techniques from the field of automated reasoning to bear on a rather different problem domain from that which motivated their development; secondly in that investigating such hard problems leads us to push the limits of what our systems have achieved; finally in that it involves us in serious philosophical issues concerning essentially computational proofs.
These are the opening paragraphs of the paper: J Slaney. The program FINDER takes as input a set of clauses in a many-sorted first order language, together with specifications of finite cardinalities of the domains for the sorts, and generates interpretations on the given domains which satisfy all of the clauses. Thus it simply finds finite models of arbitrary first order theories. It does not treat the clauses as executable statements, so for example it imposes no order on them and there is no "flow of control". Hence its semantics are very declarative. The clauses are made ground by instantiating to the given domains, and these ground instances regarded as defining the constraint satisfaction problem of evaluating the function symbols of the language across the interpretation domains. Formally, the inference mechanism it uses is ground tableau-style reasoning, driven by case analysis as is natural to such constraint satisfaction problems, with a combination of (ground) unit resolution to extend the tableau branches and a form of negative hyper-resolution to generate additional constraints during the search. Case analysis is performed on the implicit positive clauses which define the search space, the choice at each point being such as to minimise splitting of the branch. It is appropriate to see the logic as related to the Davis-Putnam algorithm. The inference process is opaque to the user. FINDER can produce a single model, to demonstrate the existence of a solution, or can enumerate all models in its (necessarily finite) search space. It is also possible to use output from FINDER as input for another FINDER job. One use of this is to select from the models of a theory only those which do not have some further property such as the definability of some function.
The Crisis in Finite Mathematics: Automated Reasoning as Cause and Cure This is the abstract of the paper John Slaney. This is an invited talk presented to CADE in Nancy (France) in June 1994. It is noted that increasing reliance on computation is causing disquiet in the field of finite mathematics. Recent research in the theory of quasigroups is examined as an example. The conceptual issues concerning essentially computer-generated proofs are examined, and it is suggested that Automated Reasoning research especially in proof checking offers the best chance for alleviation of the difficulties. This talk was an updated version of the paper with Fujita and Stickel in Computers and Mathematics with Applications which appeared the following year but was written earlier.
Automatic Generation of Some Results in Finite Algebra This is the abstract of the paper Masayuki Fujita, John Slaney and Frank Bennett. This is a report of the application of the Model Generation Theorem Prover developed at ICOT to problems in the theory of finite quasigroups. Several of these problems were previously open. In this paper, we discuss our theorem proving methods related to those of the existing provers SATCHMO (Manthey, Bry) and OTTER (McCune), and note how parallel processing on the ICOT Parallel Inference Machines was used to obtain high speeds. We then present and discuss our machine-aided investigation of seven problems concerning the existence of types of quasigroup. Winner of the Publishers' Prize for best paper at IJCAI-13.
Dr J K Slaney Phone (Aus.): (026) 125 8607 Theory Group Phone (Int.): +61 26 125 8607 Research School of Computer Science Fax (Aus.): (026) 125 8651 Australian National University Fax (Int.): +61 26 125 8651 Canberra, ACT, 0200, AUSTRALIA |