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(log n))-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).
展开▼
