[comp.theory] generating 3sat of known difficulty

richardh@syma.sussex.ac.uk (Richard John Hall) (09/25/90)

In order to test some probabilistic approaches to handling 3SAT
problems I require a simple means of generating sample 3tuple sets
of known (or at least relative) 'difficulty' ie how many
complete solutions exist, and if possible measures of
number of near-complete partial solutions.

Any suggestions, particularly if derived from real-world
applications, would be welcomed.


Richard J. Hall

pwp@iuvax.cs.indiana.edu (Paul Purdom) (09/26/90)

Random SAT problems tend to be difficult for all algorithms when the
parmeters are set so that the average number of solutions per problem is
about 1. When the problems have lots of solutions, methods that look for the
most promising setting of the variables have a good chance of finding a
solution. When the problems almost never have a solution, backtracking has a
good chance of demostrating the lack of solutions. In the case of random 3SAT
each clause knocks out 1/8 of the solution space, so a problem with t clauses
and v variables will have 2^v (7/8)^t solutions on the average. Problems with
t=5.19v should be particularly difficult.

You can find much of what is known about random SAT problems reading the
references and article in ``Random Satisfiabilty Problems'', Proceedings of
the International Workshop on Discrete Algorithms and Complexity, The
Insititue of Electronic, Information and Communication Engineers, Tokyo
Japan, (1989) pp 253--260. An easier to find article is ``Exponential Average
Time for the Pure Literal Rule'', SIAM J. Comput. 18 (1989) pp 409-418.
Neither of these articles deal with 3SAT in particular, but they reference
articles that do. Somewhat more is known about random SAT problems where is
clause length is not fixed.