Satisfiability testing for boolean formulas using Δ-trees

被引:0
|
作者
Gutiérrez G. [1 ]
De Guzmán I.P. [1 ]
Martínez J. [1 ]
Ojeda-Aciego M. [1 ]
Valverde A. [1 ]
机构
[1] Dept. Matemática Aplicada, Universidad de Málaga, 29080 Málaga
关键词
Algorithms and data structures; Automated deduction;
D O I
10.1023/A:1020530109551
中图分类号
学科分类号
摘要
The tree-based data structure of Δ-tree for propositional formulas is introduced in an improved and optimised form. The Δ-trees allow a compact representation for negation normal forms as well as for a number of reduction strategies in order to consider only those occurrences of literals which are relevant for the satisfiability of the input formula. These reduction strategies are divided into two subsets (meaning- and satisfiability-preserving transformations) and can be used to decrease the size of a negation normal form A at (at most) quadratic cost. The reduction strategies are aimed at decreasing the number of required branchings and, therefore, these strategies allow to limit the size of the search space for the SAT problem. © 2002 Kluwer Academic Publishers.
引用
收藏
页码:85 / 112
页数:27
相关论文
共 50 条
  • [1] Reduction theorems for boolean formulas using Δ-trees
    Gutiérrez, G
    de Guzmán, IP
    Martínez, J
    Ojeda-Aciego, M
    Valverde, A
    [J]. LOGICS IN ARTIFICIAL INTELLIGENCE, 2000, 1919 : 179 - 192
  • [2] The Connectivity of Boolean Satisfiability: Dichotomies for Formulas and Circuits
    Schwerdtfeger, Konrad W.
    [J]. THEORY OF COMPUTING SYSTEMS, 2017, 61 (02) : 263 - 282
  • [3] The Connectivity of Boolean Satisfiability: Dichotomies for Formulas and Circuits
    Konrad W. Schwerdtfeger
    [J]. Theory of Computing Systems, 2017, 61 : 263 - 282
  • [4] Algorithms for Testing Satisfiability Formulas
    Marin Vlada
    [J]. Artificial Intelligence Review, 2001, 15 : 153 - 163
  • [5] Algorithms for testing satisfiability formulas
    Vlada, M
    [J]. ARTIFICIAL INTELLIGENCE REVIEW, 2001, 15 (03) : 153 - 163
  • [6] Representing Boolean formulas by using trees of implicants and implicates
    Gutiérrez, G
    de Guzmán, IP
    Martínez, J
    Ojeda-Aciego, M
    Valverde, A
    [J]. PROCEEDINGS OF THE FIFTH JOINT CONFERENCE ON INFORMATION SCIENCES, VOLS 1 AND 2, 2000, : 551 - 554
  • [7] ALGORITHMS FOR TESTING THE SATISFIABILITY OF PROPOSITIONAL FORMULAS
    GALLO, G
    URBANI, G
    [J]. JOURNAL OF LOGIC PROGRAMMING, 1989, 7 (01): : 45 - 61
  • [8] The Helly property and satisfiability of Boolean formulas defined on set families
    Chepoi, Victor
    Creignou, Nadia
    Hermann, Miki
    Salzer, Gernot
    [J]. EUROPEAN JOURNAL OF COMBINATORICS, 2010, 31 (02) : 502 - 516
  • [9] Partitioning methods for satisfiability testing on large formulas
    Park, TJ
    Van Gelder, A
    [J]. INFORMATION AND COMPUTATION, 2000, 162 (1-2) : 179 - 184
  • [10] Testing the Satisfiability of Formulas in Separation Logic with Permissions
    Peltier, Nicolas
    [J]. AUTOMATED REASONING WITH ANALYTIC TABLEAUX AND RELATED METHODS, TABLEAUX 2023, 2023, 14278 : 427 - 445