02/02/2021

Satisfiability and Algorithms for Non-uniform Random k-SAT

Oleksii Omelchenko, Andrei Bulatov

Keywords:

Abstract Paper Similar Papers

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.

The video of this talk cannot be embedded. You can watch it here:
https://slideslive.com/38948612
(Link will open in new window)
 0
 0
 0
 0
  Share    
This is an embedded video. Talk and the respective paper are published at AAAI 2021 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd Characters remaining: 140

Similar Papers

 0
 0
 0
 0
 2:54 
 1
 0
 0
 0
 2:43 
 0
 0
 0
 0
 7:55 
 0
 0
 0
 0
 2:54 
 0
 0
 0
 0
 3:22 
 0
 0
 0
 0
 8:56 
 0
 0
 0
 0
 15:05 
 0
 0
 0
 0
 3:48 
 0
 0
 0
 0
 10:52 
 0
 0
 0
 0
 4:43 
 0
 0
 0
 0
 14:06 
 0
 0
 0
 0
 12:31 
 0
 0
 0
 0
 4:46 
 0
 0
 0
 0
 20:50 
 0
 0
 0
 0
 10:46 
 0
 0
 0
 0
 14:50 
 0
 0
 0
 0
 14:56 
 0
 0
 0
 1
 5:11 
 0
 0
 0
 0
 15:58 
 0
 0
 0
 0
 8:36 
 0
 0
 0
 0
 13:14 
 0
 0
 0
 0
 15:30 
 0
 0
 0
 0
 2:56 
 0
 0
 0
 0
 20:05 
 0
 0
 0
 0
 12:52 
 0
 0
 0
 0
 3:17 
 0
 0
 0
 0
 11:28 
 0
 0
 0
 0
 3:01 
 0
 0
 0
 0
 15:15 
 0
 0
 0
 0
 15:16 
 0
 0
 0
 0
 16:22 
 0
 0
 0
 0
 3:22 
 0
 0
 0
 0
 5:30 
 0
 0
 0
 0
 3:26 
 0
 0
 0
 0
 17:26 
 0
 0
 0
 0
 5:17 
 0
 0
 0
 0
 3:07 
 0
 0
 0
 0
 3:18 
 0
 0
 0
 0
 12:48 
 0
 0
 0
 0
 1:01