Satisfiability and Algorithms for Non-uniform Random k-SAT

Authors

  • Oleksii Omelchenko Simon Fraser University
  • Andrei Bulatov Simon Fraser University

Keywords:

Satisfiability

Abstract

Solving Satisfiability is at the core of a wide range of applications from Knowledge Representation to Logic Programming to Software and Hardware Verification. One of the models of Satisfiability, the Random Satisfiability problem, has received much attention in the literature both, as a useful benchmark for SAT solvers, and as an exciting mathematical object. In this paper we tackle a somewhat nonstandard type of Random Satisfiability, the one where instances are not chosen uniformly from a certain class of instances, but rather from a certain nontrivial distribution. More precisely, we use so-called Configuration Model, in which we start with a distribution of degrees (the number of occurrences) of a variable, sample the degree of each variable and then generate a random instance with the prescribed degrees. It has been proposed previously that by properly selecting the starting distribution (to be, say, power law or lognorm) one can approximate at least some aspect of `industrial' instances of SAT. Here we suggest an algorithm that solves such problems for a wide range of degree distributions and obtain a necessary and a sufficient condition for the satisfiability of such formulas.

Downloads

Published

2021-05-18

How to Cite

Omelchenko, O., & Bulatov, A. (2021). Satisfiability and Algorithms for Non-uniform Random k-SAT. Proceedings of the AAAI Conference on Artificial Intelligence, 35(5), 3886-3894. Retrieved from https://ojs.aaai.org/index.php/AAAI/article/view/16507

Issue

Section

AAAI Technical Track on Constraint Satisfaction and Optimization