Scale-Free Random SAT Instances
Carlos Ans\'otegui, Maria Luisa Bonet, Jordi Levy

TL;DR
This paper introduces a scale-free model for generating SAT instances with properties similar to real-world problems, revealing phase transition phenomena and unsatisfiability conditions based on a power-law distribution of variable occurrences.
Contribution
It proposes a novel scale-free random SAT generation model using a power-law distribution, extending classical models and analyzing phase transitions and unsatisfiability in these instances.
Findings
Existence of a SAT-UNSAT phase transition for scale-free 2-SAT when 5<1/2
High probability of unsatisfiability when clauses exceed 5n^{(1-5)k}
Model generates instances similar to industrial SAT problems
Abstract
We focus on the random generation of SAT instances that have properties similar to real-world instances. It is known that many industrial instances, even with a great number of variables, can be solved by a clever solver in a reasonable amount of time. This is not possible, in general, with classical randomly generated instances. We provide a different generation model of SAT instances, called \emph{scale-free random SAT instances}. It is based on the use of a non-uniform probability distribution to select variable , where is a parameter of the model. This results into formulas where the number of occurrences of variables follows a power-law distribution where . This property has been observed in most real-world SAT instances. For , our model extends classical random SAT instances. We prove the…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Database Systems and Queries · Distributed systems and fault tolerance · Optimization and Search Problems
