🚀 go-pugleaf

Hi everyone,

I'd greatly appreciate any pointers to approximation algorithms for the
following NP-complete problem:

Given an unweighted, undirected graph G, find a small set of _nodes_
such that removing these nodes disconnects the graph into several
components of roughly equal size.

Most algorithms I've seen for disconnecting a graph into balanced chunks
work by removing edges, not nodes.

Here is what I plan to use this for -- if this makes no sense, please
tell me:

I need to solve some large instances of UNSAT.  Backtracking algorithms
such as Davis-Putnam don't work very well on formulas with many
variables.  Could they be helped as follows: given a CNF Boolean
formula, make a graph G with one node per variable, and with an edge
between two nodes if their variables appear in some common clause.  Find
a small set of nodes whose removal disconnects G; then run DP, forcing
it to split on the variables in this set (in any order, so heuristics
for ordering the variables partially apply).  When all variables in this
set have been assigned values (either by splitting or by unit
propagation), the problem decomposes into several smaller instances;
solving them separately should be easier than solving them together as
one problem.

There are obviously problems with this, e.g. hard instances of SAT
probably don't have a small vertex separator; perhaps subproblems
obtained by partial assignments do, but then the separation algorithm
has to be run many times.  Hopefully, for some structured instances
these problems aren't too severe.  Are there other noticeable problems?

Thanks for help,

Ilya
ilya_shl@mit.edu
(please reply directly to me as well as to the newsgroup)