SATPin : Axiom Pinpointing for Lightweight Description Logics Through Incremental SAT
- PDF / 860,497 Bytes
- 6 Pages / 595.276 x 790.866 pts Page_size
- 54 Downloads / 172 Views
SYSTEMS DESCRIPTION
SATPin: Axiom Pinpointing for Lightweight Description Logics Through Incremental SAT Norbert Manthey1 · Rafael Peñaloza2 · Sebastian Rudolph1 Received: 29 November 2019 / Accepted: 28 May 2020 © Gesellschaft für Informatik e.V. and Springer-Verlag GmbH Germany, part of Springer Nature 2020
Abstract One approach to axiom pinpointing (AP) in description logics is its reduction to the enumeration of minimal unsatisfiable subformulas, allowing for the deployment of highly optimized methods from SAT solving. Exploiting the properties of AP, we further optimize incremental SAT solving, resulting in speedups of several orders of magnitude: through persistent incremental solving the solver state is updated lazily when adding clauses or assumptions. This adaptation consistently improves the runtime of the tool by an average factor of 3.8, and a maximum of 38. SATPin, our system, was tested over large biomedical ontologies and performed competitively. Keywords Pinpointing · SAT · Description logics
1 Introduction Axiom pinpointing (AP) is the task of identifying ontology axioms responsible for a logical consequence. It is used to understand and correct modeling errors in very large ontologies. For example, the 2007 version of Snomed incorrectly implied that amputations of finger were amputations of arm. Automated AP tools helped identify the 6 axioms (from ∼300, 000 ) causing this error [2] and change the modelling strategy followed by the developers of Snomed, to avoid causing it again [4]. AP has numerous applications, e.g. in context-based, error-tolerant reasoning [5, 10], and reasoning with probabilities, preferences, and provenance [7, 17, 18]. For EL+ [3], Sebastiani and Vescovi reduce AP to propositional minimal unsatisfiable subformula enumeration, exploiting SAT developments (e.g., clause learning, twowatched-literal data structure) to build efficient AP systems. * Rafael Peñaloza [email protected] Norbert Manthey nmanthey@conp‑solutions.com Sebastian Rudolph sebastian.rudolph@tu‑dresden.de 1
Technische Universität Dresden, Dresden, Germany
University of Milano-Bicocca, Milan, Italy
2
We build on this idea and identify new enumeration optimizations based on the specific shape of the propositional formula constructed. Incremental SAT solving, partial restarts, and an improved search space pruning strategy can considerably increase the efficiency of AP. While searchspace pruning via clause learning is known in SAT, it has never been used for AP. Partial restarts are also used in SAT, but not for consecutive calls to a SAT solver in incremental SAT solving. We introduce persistent incremental solving, a lazy approach preserving relevant information between runs, which has applications way beyond AP. We also use assumption prefetching, which modifies the testing order of the assumption literals aiming detecting conflicts earlier. Our Minisat-based SATPin system uses these optimizations. Experiments show that SATPin is efficient for AP over large inputs. We compare SATPin and i
Data Loading...
