Implicates and prime implicates in Random 3-SAT

AbstractIt has been observed previously that Random 3-SAT exhibits a phase transition at a critical ratio of constraints to variables, where the average frequency of satisfiability falls abruptly from near 1 to near 0. In this paper we look beyond satisfiability to implicates and prime implicates of non-zero length and show experimentally that, for any given length, these exhibit their own phase transitions. All of these phase transitions appear to share the same critical point as the well-known satisfiability phase transition. We also find a rich, regular pattern, in which phase transitions for longer implicates or prime implicates are less steep at a given problem size and all the phase transitions sharpen with increasing problem size.Implicates correspond in a one-to-one way to nogoods, and prime implicates correspond similarly to minimal nogoods. Knowledge about these phase transitions helps us to understand more about the behavior of search algorithms and knowledge compilation approaches in the context of Random 3-SAT