Learning the Right Expansion-ordering Heuristics for Satisfiability Testing in OWL Reasoners
Web Ontology Language (OWL) reasoners are used to infer new logical relations from ontologies. While inferring new facts, these reasoners can be further optimized, e.g., by properly ordering disjuncts in disjunction expressions of ontologies for satisfiability testing of concepts. Different expansion-ordering heuristics have been developed for this purpose. The built-in heuristics in these reasoners determine the order for branches in search trees while each heuristic choice causes different effects for various ontologies depending on the ontologies' syntactic structure and probably other features as well. A learning-based approach that takes into account the features aims to select an appropriate expansion-ordering heuristic for each ontology. The proper choice is expected to accelerate the reasoning process for the reasoners. In this paper, the effect of our methodology is investigated on a well-known reasoner that is JFact. Our experiments show the average speedup by a factor of one to two orders of magnitude for satisfiability testing after applying learning methodology for selecting the right expansion-ordering heuristics.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Learning Local Search Heuristics for Boolean Satisfiability
We present an approach to learn SAT solver heuristics from scratch through deep reinforcement learning with a curriculum. In particular, we incorporate a graph neural network in a stochastic local search algorithm to act…
Deep Reinforcement LearningGraph Neural Networkreinforcement-learningReinforcement Learning+2Learning Interpretable Heuristics for WalkSAT
Local search algorithms are well-known methods for solving large, hard instances of the satisfiability problem (SAT). The performance of these algorithms crucially depends on heuristics for setting noise parameters and s…
reinforcement-learningAlgorithmically generating new algebraic features of polynomial systems for machine learning
There are a variety of choices to be made in both computer algebra systems (CASs) and satisfiability modulo theory (SMT) solvers which can impact performance without affecting mathematical correctness. Such choices are c…
BIG-bench Machine LearningDetection of Planted Solutions for Flat Satisfiability Problems
We study the detection problem of finding planted solutions in random instances of flat satisfiability problems, a generalization of boolean satisfiability formulas. We describe the properties of random instances of flat…
Two-sample testingGenerating from Discrete Distributions Using Diffusions: Insights from Random Constraint Satisfaction Problems
Generating data from discrete distributions is important for a number of application domains including text, tabular data, and genomic data. Several groups have recently used random $k$-satisfiability ($k$-SAT) as a synt…