Nadia Creignou ; Reinhard Pichler ; Stefan Woltran - Do Hard SAT-Related Reasoning Tasks Become Easier in the Krom Fragment?

lmcs:4091 - Logical Methods in Computer Science, October 31, 2018, Volume 14, Issue 4 - https://doi.org/10.23638/LMCS-14(4:10)2018
Do Hard SAT-Related Reasoning Tasks Become Easier in the Krom Fragment?Article

Authors: Nadia Creignou ; Reinhard Pichler ; Stefan Woltran

    Many reasoning problems are based on the problem of satisfiability (SAT). While SAT itself becomes easy when restricting the structure of the formulas in a certain way, the situation is more opaque for more involved decision problems. We consider here the CardMinSat problem which asks, given a propositional formula $\phi$ and an atom $x$, whether $x$ is true in some cardinality-minimal model of $\phi$. This problem is easy for the Horn fragment, but, as we will show in this paper, remains $\Theta_2$-complete (and thus $\mathrm{NP}$-hard) for the Krom fragment (which is given by formulas in CNF where clauses have at most two literals). We will make use of this fact to study the complexity of reasoning tasks in belief revision and logic-based abduction and show that, while in some cases the restriction to Krom formulas leads to a decrease of complexity, in others it does not. We thus also consider the CardMinSat problem with respect to additional restrictions to Krom formulas towards a better understanding of the tractability frontier of such problems.


    Volume: Volume 14, Issue 4
    Published on: October 31, 2018
    Accepted on: August 23, 2018
    Submitted on: November 27, 2017
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Fixed-Parameter Tractability in Artificial Intelligence and Reasoning (FAIR); Funder: Austrian Science Fund (FWF); Code: P 25518
    • Decodyn: Treating Hard Problems with Decomposition and Dynamic Programming; Funder: Austrian Science Fund (FWF); Code: Y 698
    • Fragment-Driven Belief Change; Funder: Austrian Science Fund (FWF); Code: P 25521

    Consultation statistics

    This page has been seen 1130 times.
    This article's PDF has been downloaded 289 times.