A hybrid method for probabilistic satisfiability

Pavel Klinov, Bijan Parsia, Nikolaj Bjørner (Editor), Viorica Sofronie-Stokkermans (Editor)

    Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

    Abstract

    Determining satisfiability of sets of formula formulated in a Nilsson style probabilistic logic (PSAT) by reduction to a system of linear (in)equations has been extensively studied, esp. in the propositional setting. The basic technique for coping with the potentially exponentially large (in terms of the formulae) linear system is column generation, which has been successful (in various forms) in solving problems of around 1000 formulae. Common to existing techniques is that the column generation model explicitly encodes all classical, i.e., non-probabilistic, knowledge. In this paper we introduce a straightforward but new hybrid method for PSAT that makes use of a classical solver in the column generation process. The benefits of this technique are twofold: first, we can, in practice, accommodate inputs with significantly larger classical parts, and thus which are overall larger, and second, we can accommodate inputs with supra-propositional classical parts, such as propositionally complete description logics. We validate our approach with an extensive series of experiments which show that our technique is competitive with traditional non-hybrid approaches in spite of scaling the expressivity of the classical part to the description logic SROIQ. © 2011 Springer-Verlag Berlin Heidelberg.
    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.
    EditorsNikolaj Bjørner, Viorica Sofronie-Stokkermans
    PublisherSpringer Nature
    Pages354-368
    Number of pages14
    Volume6803
    ISBN (Print)9783642224379, 978-3-642-22438-6
    DOIs
    Publication statusPublished - 2011
    Event23rd International Conference on Automated Deduction, CADE 23 - Wroclaw
    Duration: 1 Jul 2011 → …

    Conference

    Conference23rd International Conference on Automated Deduction, CADE 23
    CityWroclaw
    Period1/07/11 → …

    Keywords

    • column generation
    • probabilistic satisfiability

    Fingerprint

    Dive into the research topics of 'A hybrid method for probabilistic satisfiability'. Together they form a unique fingerprint.

    Cite this