Usmeravanje pretrage u automatskom dokazivanju teorema

U ovom radu se razmatra problem usmeravanja pretrage u automatskom dokazivanju teorema. Rad se sastoji od dva dela čija je dodirna tačka CDCL sistem pretrage, koji se intenzivno koristi kod modernih SAT rešavača. U prvom delu rada razmatran je problem jednostavnog usmeravanja pretrage | izborom rešavača, njegovih heuristika i njihovih parametara, a u zavisnosti od svojstava instance koju je potrebno rešiti. Osnova predloženih metoda za izbor algoritama je sintaksna sličnost formula koja se odražava na njihovu grafovsku strukturu. Ova sličnost je prvi put pouzdano ustanovljena i analizirana pomoću originalne mere sličnosti grafova (koja se pokazala korisnom i u drugim domenima). Praktični pristupi merenju sličnosti formula se zbog računske efikasnosti ipak zasnivaju na numeričkim atributima iskaznih formula. Predložene su dve jednostavne metode izbora algoritma zasnovane na algoritmu k najbližih suseda. Prva tehnika, ArgoSmArT se zasniva na klasifikaciji instance u jednu od unapred zadatih familija za koje su poznati algoritmi koji ih efikasno rešavaju. Instanca se rešava algoritmom koji odgovara familiji u koju je instanca klasifikovana. Druga tehnika, ArgoSmArT k-NN se zasniva na nalaženju nekoliko sličnih instanci u trening skupu za koje je poznato vreme rešavanja pomoću svih algoritama kojima sistem raspolaže. Instanca se rešava algoritmom koji se najbolje ponaša na pronađenim instancama. Tehnika ArgoSmArT je pogodnija za izbor konfiguracije SAT rešavača, a ArgoSmArT k-NN za izbor samog SAT rešavača. Tehnika ArgoSmArT k-NN se pokazala značajno efikasnijom od najvažnijeg i pritom vrlo složenog sistema za izbor SAT rešavača i sistema SATzilla. Pored problema izbora KNF SAT rešavača i njihovih heuristika, razmatran je i problem izbora ne-KNF SAT rešavača u kojem fokus nije bio na tehnikama izbora rešavača, pošto se predložene tehnike direktno primenjuju i na taj problem, već na atributima kojima se ne-KNF instance mogu opisati, a koji do sad nisu predloženi. Rezulta
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 classication of instance in one of the predened families for which the ecient algorithms are known. The instance is solved by algorithm corresponding to the family to which the instance was classied. 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 conguration selection of a SAT solver, and ArgoSmArT k-NN for SAT solver selection. ArgoSmArT k-NN technique showed to be more ecient 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