This is from the Introduction to the paper:
Anbulagan, Duc Nghia Pham, John Slaney and Abdul Sattar.
Boosting SLS Using Resolution.
In Benhamou, Jussinen and O'Sullivan (eds), Trends in Constraint Programming : 283-289.
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.
Lookahead Saturation with Restriction for SAT.
Proceedings of the 11th International Conference on Principles and Practice of Constraint Programming (CP-2005) : 727-731.
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.
Old Resolution Meets Modern SLS.
Proceedings of the 20th National Conference of the American Association for Artificial Intelligence (AAAI-2005) : 354-359.
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.
Automated Reasoning and Exhaustive Search: Quasigroup Existence Problems.
Computers and Mathematics with Applications 29 (1995): 115-132.
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.
FINDER, Finite Domain Enumerator: System Description.
Proceedings of the twelfth Conference on Automated Deduction (CADE-12) (1994): 798-801.
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.
The Crisis in Finite Mathematics: Automated Reasoning as Cause and Cure.
Proceedings of the twelfth Conference on Automated Deduction (CADE-12) (1994): 1-13.
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.
Automatic Generation of Some Results in Finite Algebra.
Proceedings of the thirteenth International Joint Conference on Artificial Intelligence (IJCAI-13) (1993): 52-57.
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.
Automated Reasoning Group
Computer Sciences Laboratory
Research School of Information Sciences and Engineering
Australian National University