Under de senaste två decennierna har modal- och beskrivningslogik tillämpats på många områden inom datavetenskap, inklusive kunskapsrepresentation, formell verifiering, databasteori, distribuerad databehandling och, på senare tid, semantisk webb och ontologier. Av denna anledning har problemet med automatiserade resonemang i modal- och beskrivningslogik grundligt undersökts. I synnerhet har många metoder föreslagits för att effektivt hantera tillfredsställandet av kärnan normal modal logik K m, och dess notational variant, beskrivningen logik ALC. Även enkel struktur, K m /ALC är beräkning mycket svårt att resonera på, dess tillfredsställelse är PSpace-komplett. I detta dokument börjar vi utforska idén om att utföra automatiska resonemangsuppgifter i modal och beskrivningslogik genom att koda dem till SAT, så att hanteras av toppmoderna SAT-verktyg; som med de flesta tidigare metoder, vi börjar vår undersökning från tillfredsställande i K m. Vi föreslår en effektiv kodning, och vi testar den på en omfattande uppsättning riktmärken, jämföra metoden med de viktigaste state-of-the-art verktyg som finns tillgängliga. Även om kodningen nödvändigtvis är i värsta fall exponentiell, konstaterar vi från våra experiment att detta tillvägagångssätt i praktiken kan hantera de flesta eller alla problem som är inom räckhåll för de andra tillvägagångssätten, med prestationer som är jämförbara med, eller till och med bättre än, de nuvarande toppmoderna verktygen. Under de senaste två decennierna har modal- och beskrivningslogik gett en viktig ram för många tillämpningar inom många områden inom datavetenskap, däribland artificiell intelligens, formell verifiering, databasteori, distribuerad datorteknik och, på senare tid, semantisk webb- och ontologi. Av denna anledning, problemet med automatiserat resonemang i modal och beskrivning logik har grundligt undersökts (t.ex., Fitting, 1983; Ladner, 1977; Baader & Hollunder, 1991; Halpern & Moses, 1992; Baader, Franconi, Hollunder, Nebel, & Profitlich, 1994; Massacci, 2000). Framför allt har forskningen inom modal- och beskrivningslogik följt två parallella vägar fram till Schilds seminala arbete (1991), som visade att den centrala modallogiken K m och kärnbeskrivningslogiken ALC är en notational variant av den andra. Sedan dess har liknande resultat producerats för en massa andra logiker, så att de två forskningslinjerna i dag mestadels har slagits samman till ett enda forskningsflöde. Många tillvägagångssätt har föreslagits för ett effektivt resonemang i modal- och beskrivningslogiken, som utgår från problemet med att kontrollera tillfredsställelsen i den grundläggande normala modallogiken K m och i dess notationella variant, beskrivningslogiken ALC (nedan helt enkelt "K m"). Vi klassificerar dem enligt följande.  • Den "klassiska" tabellau-baserade metoden (Fitting, 1983; Baader & Holler, 1991; Massacci, 2000) bygger på byggandet av propositionella tablå grenar, som återkommer på efterfrågan genom att generera efterföljande noder i en kandidat Kripke modell. Kris (Baader & Hollunder, 1991; Baader et al., 1994), Crack (Franconi, 1998), LWB (Balsiger, Heuerding, & Schwendimann, 1998) var bland de viktigaste representativa verktygen för detta tillvägagångssätt. • Den DPLL-baserade metoden, 2000 skiljer sig från den tidigare i huvudsak i det faktum att en Davis-Putnam-Logemann-Loveland (DPLL) förfarande, som behandlar modal subformulas som förslag, används i stället för den klassiska propositions tabaux förfarande på varje bonivå av modal operatörer. KSAT (Giunchiglia & Sebastiani, 1996), ESAT (Giunchiglia, Giunchiglia, & Tacchella, 2002) och *SAT (Tacchella, 1999) är de representativa verktygen för detta tillvägagångssätt. Dessa två tillvägagångssätt slogs samman till den "moderna" tablåbaserade metoden, som har utvidgats till att fungera med mer uttrycksfulla beskrivningslogik och för att ge mer sofistikerade resonemangsfunktioner. Bland de verktyg som använder detta tillvägagångssätt minns vi • Den CSP-baserade metoden (Brand, Gennari, & de Rijke, 2003) skiljer sig från de tabellauxbaserade och DPLL-baserade de flesta i det faktum att en CSP (Constraint Satisfaction Problem) motor används i stället för tabellaux/DPLL. KCSP är det enda representativa verktyget för detta tillvägagångssätt. • I den inversa metoden (Voronkov, 1999 (Voronkov,, 2001 ) är ett sökförfarande baserat på den "inverterade" versionen av en sekventiell kalkyl (som kan ses som en modal version av propositionsupplösning). K K (Voronkov, 1999) är det enda representativa verktyget för detta tillvägagångssätt. • I Automata-teoretisk metod, (en symbolisk representation baserad på BDDsBinary Decision Diagrams -of) en trädautomaton som accepterar alla träd modeller av inmatningsformeln är implicit byggd och kontrolleras för tomhet (Pan, Sattler, & Vardi, 2002; Pan & Vardi, 2003). KBDD (Pan & Vardi, 2003) är det enda representativa verktyget för detta tillvägagångssätt. 1. Vad är det för fel på dig? Lägg märke till att det inte finns någon allmän överenskommelse om terminologin "tableaux-based" och "DPLL-based". T.ex., verktyg som FATT, DLP och Racer kallas oftast "tableau-baserad", även om de använder en DPLL-liknande algoritm istället för propositionstabell för att hantera den propositionella komponenten i resonemang (Horrocks, 1998; Patel-Schneider, 1998; Horrocks & Patel-Schneider, 1999; Haarslev & Moeller, 2001 ). 344 • Pan och Vardi (2003) presenterade också en kodning av K-tillfredsställelse i QBF-tillfredsställelse (som också är PSpace-komplett), kombinerat med användning av en toppmodern QBF (Quantified Boolean Formula). Vi kallar detta för tillvägagångssätt QBF-kodning. Såvitt vi vet begränsas de fyra senaste tillvägagångssätten hittills endast till tillfredsställelsen i K m, medan det translationella tillvägagångssättet har tillämpats på många olika modal- och beskrivningslogiker (t.ex. traditionella modal logik som T m och S4 m, och dynamiska modal logik) och relationskalkyl. En betydande mängd riktmärken har tagits fram för att testa de olika teknikernas effektivitet (Halpern & Moses, 1992; Giunchiglia, Roveri, & Sebastiani, 1996; Heuerding & Schwendimann, 1996; Horrocks, Patel-Schneider, & Sebastiani, 2000; Massacci, 1999; Patel-Schneider & Sebastiani, 2001. Under de senaste två decennierna har vi också bevittnat ett imponerande framsteg när det gäller effektiviteten hos propositionella tillfredsställande tekniker (SAT), som har fört med sig stora och tidigare oinskränkta problem när det gäller toppmoderna SAT-lösare. De flesta av framgångarna med SAT-teknik är motiverade av den imponerande effektivitet som uppnåtts genom det nuvarande genomförandet av DPLL-förfarandet (Davis & Putnam, 1960; Davis, Longemann, & Loveland, 1962) i dess modernaste varianter (Silva & Sakallah, 1996; Moskewicz, Madigan, Zhao, Zhang, & Malik, 2001; Eén & Sörensson, 2004). Nuvarande implementationer kan hantera formler i storleksordningen 10 7 variabler och klausuler. Som en följd av detta har många svåra verkliga problem framgångsrikt lösts genom kodning till SAT (inklusive t.ex. kretsverifiering och syntes, schemaläggning, planering, modellkontroll, automatisk testmönstergenerering, kryptoanalys, genkartläggning). Effektiva kodningar till SAT har också föreslagits för tillfredsställande problem i kvantifierfria FOL-teorier som är av intresse för formell verifiering (Strichman, Seshia, & Bryant, 2002; Seshia, Lahiri, & Bryant, 2003; Strichman, 2002). Framgångsrika SAT-kodningar inkluderar även PSpace kompletta problem, som planering (Kautz, McAllester, & Selman, 1996) och modellkontroll (Biere, Cimatti, Clarke, & Zhu, 1999). I detta dokument börjar vi utforska idén att utföra automatiska resonemang uppgifter i modal och beskrivning logik genom att koda dem till SAT, så att hanteras av state-of-art SAT-verktyg; som med de flesta tidigare metoder, vi börjar vår undersökning från tillfredsställande i K m. I teorin, uppgiften kan se hopplöst på grund av värsta fall komplexa frågor: i själva verket, med få undantag, är tillfredsställande problem i de flesta modal och beskrivning logiker inte i NP, typiskt PSpace-komplett eller ännu svårare -PSpace-komplett för K m (Ladner, 1977; Halpern & Moses, 1992) -så att kodningen är i värsta fall icke polynom. 2 I praktiken är det dock ett fåtal överväganden som gör att man inte kan bortse från att detta tillvägagångssätt kan vara konkurrenskraftigt i förhållande till den senaste tekniken. För det första, de icke-polynomiska gränserna ovan är värsta fall gränser, och formler kan ha olika beteenden från de patologiska formler som kan hittas i läroböcker. (T.ex., lägg märke till att exponenticiteten är baserad på hypotesen om obegränsadhet av någon parameter som modal djup; Halpern & Moses, 1992; Halpern, 1995.) För det andra kan vissa trick i kodningen göra det möjligt att minska storleken på den kodade formeln avsevärt. För det tredje, som beloppet för RAM 2. Vi gör implicit antagandet NP = PSpace. Sebastiani & Vescovi minne i nuvarande datorer är i ordningen GBytes och nuvarande SAT lösare kan framgångsrikt hantera enorma formler, kodningen av många modal formler (åtminstone de som inte är alltför svåra att lösa också för konkurrenterna) kan vara inom räckhåll för en SAT lösare. Slutligen, även för PSpace-komplett logik som K m, också andra state-of-the-art metoder är inte garanterade att använda polynom minne. I detta dokument visar vi att, åtminstone för tillfredsställande K m, genom att utnyttja vissa smarta optimeringar i kodningen SAT-kodning metoden blir konkurrenskraftig i praktiken med tidigare metoder. I detta avseende finns det många bidrag i detta dokument. • Vi föreslår en grundläggande kodning av K m formler till rent propositionella, och bevisa att kodning är tillfredsställande-bevarande. • Vi beskriver några optimeringar av kodning, både i form av förbehandling och förenkling på flyg. Dessa tekniker möjliggör betydande (och i vissa fall dramatiska) minskningar av storleken på de resulterande Booleska formler, och i utförandet av SAT lösaren därefter. • Vi gör en mycket omfattande empirisk jämförelse mot de viktigaste toppmoderna verktygen som finns tillgängliga. Vi visar att detta tillvägagångssätt, trots NP-vs.-PSpace-frågan, kan hantera de flesta eller alla problem som är inom räckhåll för de andra tillvägagångssätten, med prestationer som är jämförbara med, och ibland till och med bättre än, de nuvarande toppmoderna verktygen. I vårt perspektiv är detta det mest överraskande bidraget i dokumentet. • Som en biprodukt av vårt arbete får vi en empirisk utvärdering av de nuvarande verktygen för K msatisfiability som finns tillgängliga, vilket är mycket omfattande både när det gäller mängd och variation av riktmärken och antalet och representativiteten hos de utvärderade verktygen. Vi känner inte till någon annan sådan utvärdering i den senaste litteraturen. Vi betonar också att med vårt tillvägagångssätt kan kodaren kopplas samman med varje SAT-lösare på ett plug-and-play-sätt, så att man kan dra nytta av alla förbättringar i tekniken för SAT-lösare som har gjorts eller kommer att göras tillgängliga. Förnöjsamhet. Papperet är uppbyggt på följande sätt: I avsnitt 2 ger vi de nödvändiga bakgrundsbegreppen om modallogik och SAT. I Avsnitt 3 beskriver vi den grundläggande kodningen från K m till SAT. I Avsnitt 4 beskriver och diskuterar vi de viktigaste optimeringarna, och ger många exempel. I avsnitt 5 presenterar vi den empiriska utvärderingen och diskuterar resultaten. I Avsnitt 6 presenterar vi några relaterade arbeten och aktuella forskningstrender. I Avsnitt 7 avslutar vi, och beskriver några möjliga framtida evolutioner.
Forskarna presenterade också metoder för DL-resonemang genom SMT REF, som gör det möjligt att lösa DL-resonemangsproblem genom att använda effektiva toppmoderna SAT-lösare.
Automated Reasoning in Modal and Description Logics via SAT Encoding: the Case Study of K(m)/ALC-Satisfiability
{'venue': 'Journal Of Artificial Intelligence Research, Volume 35, pages 343-389, 2009', 'journal': None, 'mag_field_of_study': ['Computer Science']}