Understanding Random SAT - Beyond the Clauses-to-Variables Ratio

Sep 14, 2026

The document studies how to automatically identify properties of random SAT instances that correlate with empirical solver hardness. It applies machine learning to three SAT solvers and two instance distributions: uniform random 3-SAT with varying clause-to-variable ratios, and uniform random 3-SAT with a fixed ratio at the phase transition. The analysis shows that highly accurate predictive models can be built, then uses model inspection to determine the most useful features.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages15

Reading Time38 min

AccessFree to download

Introduction

Prior work on clause-to-variable ratio

Methodology using machine learning for empirical hardness

Goals and problem setup

Applications to SATzilla portfolio solving

Understanding Random SAT: Beyond the Clauses-to-Variables Ratio Eugene Nudelman 􀀀 , Alex Devkar􀀀 , Yoav Shoham􀀀 , and Kevin Leyton-Brown✁ ✂ Computer Science Department, Stanford University,Stanford, CA ✄ eugnud,avd,shoham☎ @[cs.stanford.edu](cs.stanford.edu)[ ](cs.stanford.edu)✆ Computer Science Department, University of British Columbia, Vancouver, BC [kevinlb@cs.ubc.ca](kevinlb@cs.ubc.ca) Abstract. It is well known that the ratio of the number of clauses to the number of variables in a random ✝-SAT instance is highly correlated with the instance's empirical hardness. We consider the problem of identifying such features of random SAT instances automatically with machine learning. We describe and analyze models for three SAT solvers􀂗kcnfs, oksolverand satz􀂗and for two different distributions of instances: uniform random 3-SAT with varying ratio of clauses-to-variables, and uniform random 3-SAT with 􀀂xed ratio of clauses-tovariables. We show that surprisingly accurate models can be built in all cases. Furthermore, we analyze these models to determine which features are most useful in predicting whether an instance will be hard to solve. Finally we discuss other applications of our models including SATzilla, a portfolio of existing SAT solvers, which competed in the 2003 and 2004 SAT competitions.3 1 Introduction SAT is among the most studied problems in computer science, representing a generic constraint satisfaction problem with binary variables and arbitrary constraints. It is also the prototypical ✞ ✟-Hard problem, and so its worst-case complexity has received much attention. Accordingly, it is not surprising that SAT has become a primary platform for the investigation of average-case and empirical complexity. Particular interest has been shown for randomly-generated SAT instances:this testbed offers a range of very easy to very hard instances for any given input size, yet the simplicity of the algorithm used to generate such instances makes them easier to understand analytically. Moreover, working on this testbed offers the opportunity to make connections toa wealth of existing work. A seminal paper by Selman, Mitchell and Levesque [13] considered the empirical performance of DPLL-type solvers running on uniform-random ✡ -SAT instances.4 It found a strong correlation between the instance's hardness and the ratio of the number of clauses to the number of variables in the instance. Furthermore, it demonstrated 3 We'd like to acknowledge very helpful assistance from Holger Hoos and Nando De Freitas, and our indebtedness to the authors of the algorithms in the SATzilla portfolio. 4 Similar, contemporaneous work on phase transition phenomena in other hard problems was performed by Cheeseman [4], among others. that the hardest region (e.g., for random 3-SAT, a clauses-to-variables ratio of roughly 4.26) corresponds exactly to a phase transition in a non-algorithm-speci􀀂c theoretical property of the instance: the probability that a randomly-generated formula having a given ratio will be satis􀀂able. This well-publicized 􀀂nding led to increased enthusiasm for the idea of studying algorithm performance experimentally, using the same tools as are used to study natural phenomena. Over the past decade, this approach has complemented more traditional theoretical worst-case analysis of algorithms, with interesting 􀀂ndings on (e.g.) islands of tractability [7], search space topologies for stochastic local search algorithms [6], backbones [12], backdoors [16] and random restarts [5] that have improved our understanding of algorithms' empirical behavior. Inspired by the success of this work in SAT and related problems, in 2001 we proposed a new methodology for using machine learning to study empirical hardness [10] . We applied this methodology to the Combinatorial Auction Winner Determination Problem (WDP)􀂗an ✞ ✟-hard combinatorial optimization problem equivalent to weighted set packing. In later work [9, 8] we extend

FAQs

What problem does the document address about random SAT instances?

It addresses how to automatically identify features of random SAT instances that predict empirical hardness using machine learning.

Which SAT solvers and instance distributions are analyzed?

It analyzes three SAT solvers (kcnfs, oksolver, and satz) on two distributions: uniform random 3-SAT with varying clause-to-variable ratios, and uniform random 3-SAT with the ratio fixed at the phase transition point.

What is the main contribution regarding predictive models and features?

The document shows that surprisingly accurate hardness prediction models can be built in all studied cases and further analyzes the models to identify which features are most useful for predicting hardness.

Sep 14, 2026

Uploaded by Berry Peter