Modular SAT-based techniques for reasoning tasks in team semantics

被引：0
|
作者：
Durand, Arnaud [1 ]
Kontinen, Juha [2 ]
Vaananen, Jouko [2 ,3 ]
机构：
[1] Univ Paris Cite, CNRS, IMJ PRG, F-75013 Paris, France
[2] Univ Helsinki, Dept Math & Stat, Helsinki, Finland
[3] Univ Amsterdam, Inst Log Language & Computat, Amsterdam, Netherlands
来源：
JOURNAL OF COMPUTER AND SYSTEM SCIENCES | 2024年 / 146卷
基金：
欧洲研究理事会; 芬兰科学院;
关键词：
Team semantics; Data complexity; Boolean satisfiability; DEPENDENCE; COMPLEXITY; LOGICS;
D O I：
10.1016/j.jcss.2024.103575
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
We study the complexity of reasoning tasks for logics in team semantics. Our main focus is on the data complexity of model checking but we also derive new results for logically defined counting and enumeration problems. Our approach is based on modular reductions of these problems into the corresponding problems of various classes of Boolean formulas. We illustrate our approach via several new tractability/intractability results. (c) 2024 The Author(s). Published by Elsevier Inc. This is an open access article under the CC BY license (http://creativecommons .org /licenses /by /4 .0/).
引用
收藏
页数：18
相关论文
共 50 条
  • [1] SAT-based procedures for temporal reasoning
    Armando, A
    Castellini, C
    Giunchiglia, E
    [J]. RECENT ADVANCES IN AI PLANNING, 2000, 1809 : 97 - 108
  • [2] Bounded Semantics of CTL and SAT-Based Verification
    Zhang, Wenhui
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, 2009, 5885 : 286 - 305
  • [3] SAT-based techniques in system synthesis
    Haubelt, C
    Teich, J
    Feldmann, R
    Monien, B
    [J]. DESIGN, AUTOMATION AND TEST IN EUROPE CONFERENCE AND EXHIBITION, PROCEEDINGS, 2003, : 1168 - 1169
  • [4] On Determining the Real Output Xs by SAT-Based Reasoning
    Elm, Melanie
    Kochte, Michael A.
    Wunderlich, Hans-Joachim
    [J]. 2010 19TH IEEE ASIAN TEST SYMPOSIUM (ATS 2010), 2010, : 39 - 44
  • [5] Using SAT-based techniques in power estimation
    Sagahyroon, Assim
    Aloul, Fadi A.
    [J]. MICROELECTRONICS JOURNAL, 2007, 38 (6-7) : 706 - 715
  • [6] Incremental Solving Techniques for SAT-based ATPG
    Tille, Daniel
    Eggersgluess, Stephan
    Drechsler, Rolf
    [J]. IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2010, 29 (07) : 1125 - 1130
  • [7] Search techniques for SAT-based Boolean optimization
    Department of Computer Engineering, American University of Sharjah, Sharjah, United Arab Emirates
    [J]. Met. Finish., 2006, 6 (436-447):
  • [8] Search techniques for SAT-based boolean optimization
    Aloul, Fadi A.
    [J]. JOURNAL OF THE FRANKLIN INSTITUTE-ENGINEERING AND APPLIED MATHEMATICS, 2006, 343 (4-5): : 436 - 447
  • [9] SAT-based decision procedures for automated reasoning: A unifying perspective
    [J]. Armando, A. (armando@dist.unige.it), 2005, Springer Verlag (2605 LNAI):
  • [10] SAT-based decision procedures for automated reasoning: A unifying perspective
    Armando, A
    Castellini, C
    Giunchiglia, E
    Giunchiglia, F
    Tacchella, A
    [J]. MECHANIZING MATHEMATICAL REASONING: ESSAYS IN HONOUR OF JORG H SIEKMANN ON THE OCCASION OF HIS 60TH BIRTHDAY, 2005, 2605 : 46 - 58
12345