Solving X3SAT Using Bipartite Graphs

Solving X3SAT Using Bipartite Graphs

I describe a method to solve certain classes of exclusive
3-SAT (X3SAT), also called exactly 1 in 3 SAT.
The method is theoretically interesting because it doesn't use resolution.
Instead, it finds bipartite subgraphs contained in certain types of graphs.
The method has a worst case of O( n * 2^(m-1) ) where m is the number of
clauses.
Despite this, the method can quickly find solutions to many X3SAT instances.
For example, this method will quickly solve instances that have many
solutions.
The method can also find all solutions to an instance.
Many methods of solving X3SAT require detailed case by case analysis.
This method is mechanically simple.
It spends most of its time finding edges in subsets of vertices.
I describe the method at:
http://home.comcast.net/~logiclab/BipartiteSolver.htm


Russell
- 2 many 2 count


.