|
Abstract:
|
In this thesis the problem of guiding search in automated theorem proving
is considered. The thesis consists of two parts that have the CDCL search
system, the system intensively used by modern SAT solvers, as their common topic.
In the rst part of the thesis a simple approach to guiding search is considered
| guiding by the selection of the solver, its heuristics, and their parameters, based
on the properties of an instance to be solved. The basis of the proposed methods
for algorithm selection is syntactical similarity of formulae which is re
ected in their
graph structure. This graph similarity is established and analyzed by using an
original graph similarity measure (which turned out to be useful in other contexts,
too). Yet, practical approaches to measuring similarity of formulae are based on their
numerical features due to the computational complexity issues. Two simple methods
for algorithm selection, based on k nearest neighbors, were proposed. The rst
technique, ArgoSmArT is based on classi cation of instance in one of the prede ned
families for which the e cient algorithms are known. The instance is solved by
algorithm corresponding to the family to which the instance was classi ed. The
second technique, ArgoSmArT k-NN is based on nding several similar instances in
the training set for which the solving times by all considered algorithms are known.
The instance is solved by the algorithm that behaves the best on those instances.
ArgoSmArT technique is better suited for con guration selection of a SAT solver,
and ArgoSmArT k-NN for SAT solver selection. ArgoSmArT k-NN technique showed
to be more e cient than the most important and very complex system for SAT
solver selection | SATzilla system. Apart from CNF SAT solver selection, the
problem of non-CNF SAT solver selection is considered. The focus was not on
solver selection techniques, since the proposed techniques are directly applicable,
but on the attributes that can be used to describe non-CNF SAT instances, which
have not been proposed earlier. The results in this domain are positive, but still
limited. The main reason for that is the lack of greater number of non-CNF SAT
solver of di erent behaviour, which is not surprising, having in mind that this kind
of solvers is in its early stage of development.
Apart from construction of e cient SAT solver selection system, the methodology
of SAT solver comparison, based on statistical hypothesis testing is proposed.
The need for such a methodology comes from great run time variations of single
instance solving by a solver, which can result in di erent SAT solver orderings when
one tries to compare their performance or rank them, as experimentally demonstrated.
The proposed methodology gives the estimate of statistical signi cance of the
performed test and the estimate of the e ect size, for instance the probability of a
solver being faster than another.
The second part of the thesis is concerned with generalizing CDCL search system
to fragments of rst order logic. The proposed system can be used as a basis for
e cient proving in some fragment if the rules of resolution and factoring are speci ed
for that fragment. These rules are de ned for an extension of coherent logic. The
soundness and completeness of the system are proved. The system has several
distinguishing features which are a consequence of previously performed analysis
of challenges in coherent logic theorem proving. The system enables rst order
reasoning, instead of ground one characteristic for all existing coherent logic provers.
Moreover, it introduces backjumps and lemma learning. The special attention in
system design was paid to the possibility of generating readable proofs by the prover
implementing the system. This possibility is one of the greatest qualities of coherent
logic, but it is not easy to achieve if CDCL search system is used. One of the
properties of the system that came from the need for generation of readable proofs
is preservation of quanti ers in proving process which is rather unusual for existing
CDCL systems. Another advantage of the proposed CDCL system is the possibility
of transfer of heuristics which are already successfully employed in SAT solving to
other domains.
Based on the proposed system, the proof procedure Calypso for extended coherent
logic was de ned which can also be used in standard coherent logic. The
extension of Rete algorithm which enables detection of con
icts and literals to be
propagated or decided is proposed. Procedure Claypso is implemented in C++. It
was evaluated on a representative coherent logic problems and it showed superior to
other coherent logic provers and also the prover Vampire, the most e cient prover
for rst order logic.
Based on the results presented in this thesis, it can be concluded that the main
hypothesis of this work, that the search system used in CDCL SAT solvers can be
signi cantly improved by simple guiding and that it can be successfully formulated
for fragments of rst order logic such as coherent logic, was con rmed and that the
concrete answers on how to do that were provided. |