Various (tableau) optimization techniques have been integrated into OWL reasoners to speed up reasoning. Many of the techniques rely on heuristics that have been manually ne tuned for achieving a good performance but might fail dramatically when encountering ontologies exhibiting unexpected design patterns. A typical example are heuristics applied to disjunctions in order to select a disjunct to be added to the tableau. Evidences indicate that the order of selecting disjuncts can have a signi cant impact on reasoning speed. Our approach presented in this paper applies machine learning to make the selection process more e ective and removes the need for manual ne tuning. We extended the OWL reasoner JFact accordingly to control the disjunct selection process. We demonstrate that one can successfully learn to choose a disjunct based on the most e ective heuristic method. As a rst step we focused on propositional SAT testing. Our results show that machine learning can speed up JFact by one to two orders of magnitude.
A large amount of research has been devoted to the design of tableau optimization techniques for Web Ontology Language (OWL) reasoning. Heuristic guided optimization techniques try to decrease the size of the search space by making better decisions while dealing with non-deterministic expansions (disjunctions). While these methods try to improve the optimization techniques, learning from these techniques has not yet been considered for helping OWL reasoners to make the best decision when applying a non-deterministic rule.
Among the many optimization techniques, semantic branching is directly a ected by the non-determinism caused by disjunctions; nevertheless, semantic branching was developed to reduce the non-deterministic cost of syntactic branching as a part of traditional tableau algorithms.
In our enhanced version of semantic branching we apply machine learning
to choose a disjunct that could have a drastic impact on reasoning speed. One
? Corresponding author
heuristic technique suggested for this purpose is to use the MOMS heuristic that
looks for a disjunct with the maximum number of occurrences in disjunctions
of minimum size [
Semantic branching uses the Davis-Putnam-Logemann Loveland (DPLL) algorithm that splits branches by making them disjoint from each other. DPLL is used to solve the satis ability problem (SAT) in propositional logic. Therefore, learning to apply the most proper order for variables while solving a SAT problem helps with the order of applying variables in semantic branching.
A SAT solver's runtime varies based on the given instance and the heuristic
algorithm used for choosing variables in each decision level. In order to solve a
SAT problem e ciently, the approach in [
In our work, we employ multinomial logistic regression too. Our approach,
however, applies machine learning to semantic branching in OWL reasoners and
not to SAT solvers. Although, propositional logic is less expressive than
Description Logic (DL) [
There also exist methods that do not consider heuristics while detecting
the best possible expansion. An optimization technique called learning-based
disjunct was introduced in [
In order to integrate our approach into JFact, for each clause in the reasoner's input, the order of variables is changed. The new order is speci ed based on the order given by solving an input as a SAT problem using machine learning; in other words, JFact uses our fully trained model to nd the new order. Thus, the clauses in each branching level of reasoning have a new order that could lead to an earlier solution. The speed improvement is caused by the reduced occurrence of backjumping due to the changes in (semantic) branching.
The remainder of the paper is as follows: Section 2 provides a brief background on semantic branching and its relation to DPLL as well as backjumping, whereas Section 3 describes how machine learning is used in our algorithm together with branching heuristics. Section 4 describes our experiments. 2
Testing the satis ability of a concept in tableau-based systems might be costly due to non-deterministic expansions. OWL/DL reasoners try to avoid such a cost by using optimization techniques that can save memory and/or time. Our learning technique has an (in)direct impact on two of these optimization techniques: semantic branching and backjumping.
Semantic Branching: Traditional tableau algorithms use a not very e cient
algorithm called syntactic branching. Due to the redundant search space, which
syntactic branching might explore, new reasoners apply semantic branching
instead [
Backjumping: This is a search reduction technique which uses dependency lists
to avoid redundant backtracking in completion graphs. Despite backtracking,
backjumping does not just backtrack from a clash to the most recent expanded
disjunction, but it also considers whether a disjunction is related to a clash by
creating a dependency set for each disjunct and labeling the concepts with sets
containing the non-deterministic choices in each branch [
As already noted, the order of applying variables in semantic branching can signi cantly a ect the resulting runtime. Based on di erent branching heuristics, variables can have di erent scores. These branching heuristics try to prune the search tree by targeting speci c variables and clauses.
The equation below determines the score of each variable (Score(Var )) by considering the score of its literals in each branch, so it could balance between the branches to increase the variable's score. The rst branch considers the positive from score(Lit +) and the second branch considers the negation from score(Lit ): Score(Var ) = score(Lit +) + score(Lit )
Choosing the variable with the highest score (Score(Var )) may save time by leading us to an earlier solution. Moreover, by knowing the scores of both literals or branches (score(Lit +) and score(Lit )), one can also choose between the branches. In our implementation, we are currently only concerned about changing the order of selecting variables in the reasoning process.
Below are the well-known branching heuristics used in our implementation. First literal The rst literal occurring in the boolean formula is returned. MOMS The literal with the maximum number of occurrences in the clauses with minimum size is considered.
MOMS (l ) = occurrences of l in minimum size clauses.
MOMSF It is the alternative of MOMS . If f (x) is the number of occurrences
of the variable x in the clauses of minimum size, we return the variable
maximizing (f (Lit +) + f (Lit )) 2 k + (f (Lit +) f (Lit )) where k is a de ned
constant. [
MAXO The literal with the maximum number of occurrences in the boolean formula has the greatest score.
MAXO (l) = number of occurrences of l in the formula.
JW The Jeroslaw-Wang chooses the literal that maximizes the following equation where nj is the number of literals in the clause Cj :
JW (l) = Pj;l2Cj 2 nj JW2 The two sided Jeroslaw-Wang is the same as JW , but to choose a variable it considers its score by adding the score of its positive and negative literals together.
DLCS It counts the number of clauses in which the literal and its negation occur in and assigns them respectively with CP and CN :
DLCS (Var ) = CP (Var ) + CN (Var ) The variable with maximum DLSC is selected. If CP CN , the positive form of variable (l) is chosen and if CP < CN , the negative form (:l) is chosen. DLSC is faster than JW .
POSIT it is similar to DLCS , but the search is only done on clauses with minimum size.
DLIS It is the same as DLCS , but it chooses the maximum value among all CP and CN values; then, it picks the variable with the maximum value. DLIS performs faster than DLCS and on some benchmarks it performs twice as fast as JW . 3.2
A learning method is applied to assign a heuristic method to each logic expression based on its features. In this study, we use logistic regression.
In comparison with linear regression, which predicts a continuous dependent variable for each independent variable (instance), logistic regression predicts a categorical dependent variable (class) for each independent variable.
The model built for logistic regression considers the dependent variable as a
conditional probability given as P (Y = 1jX = x) that indicates the probability
of choosing a speci c class (identi ed as 1) for an instance x. If the resulting
probability is more than 0.5, then the instance belongs to class 1; otherwise, it
belongs to class 0 [
The represented model for linear regression is a linear equation that relates independent variables (x with n features x1; x2; :::; xn) to dependent variables (h(x)): h(x) = wT x = Pn i=0 wixi Note that x0 = 1 and w stands for parameters or weights.
Using the same model for logistic regression leads to:
P (Y = 1jx) = wT x which is not promising, since the probability should be bounded between 0 and 1. Therefore, the modi ed equation represented for logistic regression is: P (Y = 1jx) =
ewT x 1 + ewT x Multinomial Logistic Regression If the number of classes to predict is more than two (several branching heuristics), then the logistic regression technique is called multinominal logistic regression and it is de ned by:
P (Y = Hj jx) =
ewHTj x PH0 ewHT0 x where PH P (Hjx) = 1, H = H1; H2; :::; Hj ; ::; Hk. Notice that for all k classes, the probability of an instance labeled as each of those classes will be obtained; nally, among the obtained probabilities the maximum one de nes the class that the instance belongs to.
To obtain the best value for parameters (w), the Newton-Raphson method is used to maximize the approximation of the predictor function. To obtain the best (w), Newton-Raphson uses Hessian and Gradient that are the second and rst derivative of the error function (J (w)), respectively. In our experiment, the following formula is repeated 11 times to obtain the best w (w0 is initiated with a vector of 0s): wi+1 = wi
J 0(wi)
J 00(wi)
A set of benchmarks is used as training data for this method. The training data from the benchmarks contains instances (x). To obtain a class or heuristic (yi) of each instance (xi), all heuristics are applied to the instances and for each instance the heuristic that runs fastest will be considered as the class of that instance. Afterwards, the training data pairs (xi; yi) are ready to be used for the Newton-Raphson method. While computing wHj , the training instances with class Hj will be identi ed as class 1 and others are 0.
The error function (J (w)) in logistic regression is de ned as:
J (w) =
Pm
i=1 yilog(h(xi)) + (1
yi)log(1
h(xi))
To avoid over tting, the regularized term Pim=1 wi2 is added to the cost function
(Hessian and Gradient formulas will also be changed accordingly) where is a
regularization parameter.
For our implementation and experiments, we use JFact1, which is a Java port
of the FaCT++2 reasoner [
In this experiment, we only deal with propositional logic input. Therefore, the training data contains DIMACS CNF format les to be solved with a SAT solver. We used a standard SAT solver based on the DPLL algorithm.
To verify whether providing more training data can give us more accurate results, we use a learning curve to show how increasing the number of training data can increase/decrease the accuracy of our classi er. As shown in Fig. 1, we are con dent that adding more training data will not change the accuracy of the classi er. The ten features, which have been used for our experiments, are { Number of variables (var ) 1 https://sourceforge.net/projects/jfact/ 2 https://code.google.com/archive/p/factplusplus/ 3 http://www.cs.ubc.ca/~hoos/SATLIB/benchm.html
These features are chosen based on the characteristics that play a main role
when using heuristics for solving SAT problems. Selecting too many features
may lead to over tting depending on the number of training samples.
Regularization helps to prevent over tting if there are too many |and possibly irrelevant
|features [
The nine branching heuristics used for our experiments are: FirstLiteral , MOMS , MOMF , JW , JW2 , POSIT , ZM , DLSC , and DLIS . Table 3 shows for each heuristic on how many training samples (and for what percentage) it resulted in the shortest runtime compared to the other heuristics.
Although more heuristic methods have been developed recently, none of them
is the most e ective solution for all benchmarks. For example, MOMS may only
be good for logic expressions with many binary or unary clauses [
Based on the algorithm, for each training data, the selected branching heuristic is used until the solver process is nished. The same applies for the sample tests.
The sample cases chosen as input are OWL les in conjunctive normal form.
Depending on the complexity of the input (it does not matter if it is already in
conjunctive normal form), JFact builds a directed acyclic graph (DAG) structure
of that input [
Our samples are OWL les created from CNF DIMACS format les in which a concept, which is targeted for checking its satis ability, is equal to the CNF. Since the target concept contains the whole CNF, JFact builds an explicit structure from the OWL le; therefore, targeting speci c points of the DAG structure can be done easily since all levels of the DAG structure are directly involved in building the concept. More consideration is needed when the DAG is not explicit since one needs to gure out which levels of the DAG are directly involved in building a concept, i.e., the process of checking satis ability of that concept. As an example, let us consider the following CNF DIMACS format data. p cnf 4 3 2 3 -4 1 0 -4 0 2 3 4 0
Our OWL generator builds an OWL le from the CNF DIMACS le and adds a fresh concept named D that is equivalent to the given CNF. Therefore, we get the following description logic axiom.
D (A t B t C t :E) u :E u (B t C t E)
The DAG structure built by JFact for the above axiom is 1 *TOP* 2 primconcept(urn:jfact#temp) [= 1 3 concept(ontology:#D) = 10 4 primconcept(ontology:#A) [= 1 5 primconcept(ontology:#B) [= 1 1 2 4 5 6 7 9 11 12 22,651 25,247 52,989 20,229 16,770 7,268 18,779 6,866 5,744
Here, D is a newly added de ned concept, which stands for a non-primitive concept, and it is linked to node 10. Other concepts called A, B, C, E are de ned as primconcept (stands for primitive concept). They are used to build D and are linked to the concept > (Top) as node 1. 4.2
Our experiment contains 40 sample tests with the number of clauses between 150 and 400 and the number of variables between 35 and 90. Half of the samples are satis able and half are unsatis able. The experiments were performed on a MacBook Pro with 2.2 GHz Intel Core i7, RAM 16 GB 1600 MHz DDR3 using a correspondingly modi ed version of JFact. We carried out a 7-fold cross validation on 1400 training sets with a learning accuracy of 83%.
The performance of 13 out of 40 of our sample tests are shown in Table 4. These samples with their characteristics give an adequate representation (more similar in their characteristics compared to other samples) of all 40 samples. For each sample the table lists the original runtime (no learning), the improved runtime (with learning), the number of original backjumps (no learning), the number of reduced backjumps (with learning), the runtime speedup (de ned as original runtime divided by improved runtime), the backjump reduction (de ned as the number original backjumps divided by the number of reduced backjumps), and also the number of clauses, variables, and the SAT status. Table 4 also demonstrates that there is a direct relationship between the speed improvement and the reduction in the number of backjumps. For example, for the sample number 8, the number of backjumps went from 7,699,075 down to 271,423 (reduction of 28) while the runtime improved from 106,941 milliseconds to 4,393 milliseconds (speedup of 24).
The overall performance of the algorithm is given in Table 5. It lists the maximum, minimum and mean runtime improvement in milliseconds and the corresponding speedup factors. This shows that applying learning improves the speed of satis ability checking by one to two orders of magnitude.
Moreover, the percentage of improvement based on (un)satis ability suggests that the learning technique is more successful for satis able cases. The rate of success for unsatis able and satis able input are 53.01% and 78.25%, respectively.
Since we want to achieve a signi cant runtime improvement (e.g., at least 10%), we mostly consider sample tests that perform in a su cient amount of time (e.g., at least several seconds) such that the improvement is obvious. For example, the samples with below 50 variables and 100 clauses mostly perform in less than one second; therefore, improving their speed is not our primary concern.
On the other hand, the sample number 3 from Table 4 (with 60 variables and 160 clauses) has a initial runtime of 597,447 milliseconds and the runtime is improved by 62,712 milliseconds after learning. Therefore, the percentage of improvement is 10.49%, which is still considered as good. Moreover, for the CNF les with more than 100 variables and 400 clauses, our experiments require several minutes of runtime. For example, if a sample test is executed in 5 minutes and the improvement is only 10 seconds, then the improvement percentage is only 3 percent which we do not consider as signi cant. That is also one of the reasons, that in our 40 successful sample tests we only included very few with long running times since the learning improvement is not always very signi cant.
Our implementation does not improve the runtime for every input. For one out of every ve input les (20%) the runtime is mostly unchanged or increased by less than 10%. For example, in one sample test, the runtime without learning is 502,131 milliseconds. After learning, the runtime has increased by 2.43%, which we consider as a tolerable performance loss.
To reduce the number of cases without a signi cant speedup, we believe it is a good idea to discover speci c CNF patterns where a learning improvement is not expected. For example, in one of the identi ed patterns for every clause there also exist clauses with the exact same variables of that clause but every other possible combinations of their literals. An example of such pattern is the following description logic axiom.
D (A t E t F ) u (A t :E t F ) u (A t E t :F ) u (A t :E t :F ) u (:A t E t F ) u (:A t :E t F ) u (:A t E t :F ) u (:A t :E t :F ) u (B t C) u (B t :C) u (:B t C) u (:B t :C) Note that the features such as the number of variables and clauses are close to the successful samples.
Finding these patterns can also help us to categorize OWL input to enhance the reliability of our future implementation, which will also be extended for more expressive OWL input. 5
In this paper, we focused on improving one of the well known optimization techniques for OWL reasoners called semantic branching. Even though semantic branching is guaranteed to avoid redundant search space occurring in traditional syntactic branching, machine learning techniques also help to further decrease redundant search space exploration. The task is possible by learning new orderings for applying variables in each branching level. Our algorithm has demonstrated a signi cant improvement in our sample tests.
As part of our future work, we started to expand our approach beyond propositional description logic and integrate the proper treatment of universal, existential quanti ers, and quali ed number restrictions in our machine learning approach. For instance, we started working on strategies to apply machine learning in a similar way while also considering interactions between OWL axioms.
Similar strategies could be applied to simplify OWL expressions and prepare them for machine learning. Later, for training purposes, OWL expressions could be treated as propositional logic or Quanti ed Boolean Formulas (QBF) so they can take advantage of available training sets to be solved by QBF or SAT solvers. Moreover, as already mentioned in the previous section, categorizing OWL input based on its shape and pattern could be also helpful for further exploration. Finally, we plan to consider other learning techniques such as Naive Bayes and k-Nearest Neighbor based on the features and their correlation.