Studia Logica 72 (1):85 - 112 (2002)
|Abstract||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.|
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Martin Otto (2001). Two Variable First-Order Logic Over Ordered Domains. Journal of Symbolic Logic 66 (2):685-702.
Robert Cowen & Katherine Wyatt (1993). BREAKUP: A Preprocessing Algorithm for Satisfiability Testing of CNF Formulas. Notre Dame Journal of Formal Logic 34 (4):602-606.
Frank Wolter & Michael Zakharyaschev (2001). Decidable Fragments of First-Order Modal Logics. Journal of Symbolic Logic 66 (3):1415-1438.
Adam Kolany (2010). Reversed Resolution in Reducing General Satisfiability Problem. Studia Logica 95 (3):407 - 416.
Johan van Benthem (2005). Guards, Bounds, and Generalized Semantics. Journal of Logic, Language and Information 14 (3):263-279.
Fahiem Bacchus & Toby Walsh (eds.) (2005). Theory and Applications of Satisfiability Testing: 8th International Conference, Sat 2005, St Andrews, Uk, June 19-23, 2005: Proceedings. [REVIEW] Springer.
Holger H. Hoos & David G. Mitchell (eds.) (2005). Theory and Applications of Satisfiability Testing: 7th International Conference, Sat 2004, Vancouver, Bc, Canada, May 10-13, 2004: Revised Selected Papers. [REVIEW] Springer.
Charles E. Hughes (1976). A Reduction Class Containing Formulas with One Monadic Predicate and One Binary Function Symbol. Journal of Symbolic Logic 41 (1):45-49.
Stål O. Aanderaa, Egon Börger & Harry R. Lewis (1982). Conservative Reduction Classes of Krom Formulas. Journal of Symbolic Logic 47 (1):110-130.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Total downloads1 ( #291,771 of 722,859 )
Recent downloads (6 months)0
How can I increase my downloads?