SATPin: Axiom Pinpointing for Lightweight Description Logics through Incremental SAT

Norbert MantheyNorbert Manthey, Rafael Peñaloza NyssenRafael Peñaloza Nyssen, Sebastian RudolphSebastian Rudolph

Norbert Manthey, Rafael Peñaloza Nyssen, Sebastian Rudolph
SATPin: Axiom Pinpointing for Lightweight Description Logics through Incremental SAT
Künstliche Intelligenz, 34(3):389-394, 2020

Details
Bibtex

KurzfassungAbstract
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.
Weitere Informationen unter:Further Information: Link
Projekt:Project: DeciGUT
Forschungsgruppe:Research Group: Computational LogicComputational Logic

@article{MNR2020,
  author  = {Norbert Manthey and Rafael Pe{\~{n}}aloza Nyssen and Sebastian
             Rudolph},
  title   = {SATPin: Axiom Pinpointing for Lightweight Description Logics
             through Incremental {SAT}},
  journal = {K{\"{u}}nstliche Intelligenz},
  volume  = {34},
  number  = {3},
  year    = {2020},
  pages   = {389-394},
  doi     = {10.1007/s13218-020-00669-4}
}