Abstract
We investigate theoretical and practical aspects of algorithms for CIRCUIT-SAT and SAT based on combinatorial parameters. Two such algorithms are given in [1] and [4] based on branch-width of a hypergraph and cut-width of a graph respectively. We give theoretical generalizations and improvements to the cut-width-based algorithm in [4] in terms of many other well-known width-like parameters. In particular, we have polynomial-time backtrack search algorithms for logarithmic cut-width and path-width, n O(logn)-time backtrack search algorithms for logarithmic tree-width and branch-width, and a polynomial-time regular resolution refutation for logarithmic tree-width. We investigate the effectiveness of the algorithm in [1] on practical instances of CIRCUIT-SAT arising in the context of Automatic Test Pattern Generation (ATPG).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alekhnovich, M., Razborov, A.: Satisfiability, Branch-width, and Tseitin Tautologies. In: 43rd Symp. Foundations of Computer Science (FOCS), pp. 593–603 (2002)
Bodlaender, H.L.: A Partial k-arboretum of Graphs with Bounded Treewidth. Theoretical Computer Science 209, 1–45 (1998)
Cook, W., Seymour, P.: Tour Merging via Branch-Decompistion (December 18, 2002) (manuscript)
Prasad, M.R., Chong, P., Keutzer, K.: Why is Combinatorial ATPG Efficiently Solvable for Practical VLSI Circuits? Journal of Elecrtonic Testing: Theory and Applications 17, 509–527 (2001)
Diestel, R.: Graph Theory, 2nd edn. Graduate Texts in Mathematics, vol. 173. Springer, Heidelberg (2000)
Robertson, N., Seymour, P.D.: Graph Minors X - Obstructions to Treedecomposition. Jl. Combinatorial Theory, Series B 52, 153–190 (1991)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Broering, E., Lokam, S.V. (2004). Width-Based Algorithms for SAT and CIRCUIT-SAT. In: Giunchiglia, E., Tacchella, A. (eds) Theory and Applications of Satisfiability Testing. SAT 2003. Lecture Notes in Computer Science, vol 2919. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24605-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-24605-3_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20851-8
Online ISBN: 978-3-540-24605-3
eBook Packages: Springer Book Archive