•  24
    Satisfiability Testing for Boolean Formulas Using Δ-Trees
    with G. Gutiérrez, J. Martínez, M. Ojeda-Aciego, and A. Valverde
    Studia Logica 72 (1). 2002.
    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 si…Read more
  •  64
    Satisfiability testing for Boolean formulas using δ-trees
    with G. Gutiérrez, J. Martínez, M. Ojeda-Aciego, and A. Valverde
    Studia Logica 72 (1). 2002.
    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…Read more