SATPin: Axiom Pinpointing for Lightweight Description Logics Through Incremental SAT

dc.contributor.author	Manthey, Norbert
dc.contributor.author	Peñaloza, Rafael
dc.contributor.author	Rudolph, Sebastian
dc.date.accessioned	2021-04-23T09:35:31Z
dc.date.available	2021-04-23T09:35:31Z
dc.date.issued	2020
dc.description.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.	de
dc.identifier.doi	10.1007/s13218-020-00669-4
dc.identifier.pissn	1610-1987
dc.identifier.uri	http://dx.doi.org/10.1007/s13218-020-00669-4
dc.identifier.uri	https://dl.gi.de/handle/20.500.12116/36305
dc.publisher	Springer
dc.relation.ispartof	KI - Künstliche Intelligenz: Vol. 34, No. 3
dc.relation.ispartofseries	KI - Künstliche Intelligenz
dc.subject	Description logics
dc.subject	Pinpointing
dc.subject	SAT
dc.title	SATPin: Axiom Pinpointing for Lightweight Description Logics Through Incremental SAT	de
dc.type	Text/Journal Article
gi.citation.endPage	394
gi.citation.startPage	389

Sammlungen