SATPin: Axiom Pinpointing for Lightweight Description Logics through Incremental SAT

From International Center for Computational Logic

Toggle side column

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
  • 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}
}