As a guest user you are not logged in or recognized by your IP address. You have
access to the Front Matter, Abstracts, Author Index, Subject Index and the full
text of Open Access publications.
Phase-transition in random SAT formulas is one of the properties best studied by theoretical SAT researchers. There exists a constant rk depending on k such that, if we choose randomly a k-SAT formula over n variables and m clauses, it will be satisfiable with high probability, if m/n < r, and unsatisfiable, otherwise. However, this criterion is useless in practice, because real-world or industrial instances have some properties not shown in random formulas. In the last years, several models of realistic random formulas have been proposed.
Here we discuss about the phase transition in these models, and about the size of unsatisfiability proofs. We observe that in these models, like in real-world formulas, there is not a sharp phase transition, the transition occurs for smaller values of r, and the proofs on unsatisfiable formulas are smaller than in the classical random model. We also discuss about the strategies used by modern SAT solvers to exploit these properties.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.
This website uses cookies
We use cookies to provide you with the best possible experience. They also allow us to analyze user behavior in order to constantly improve the website for you. Info about the privacy policy of IOS Press.