Analysis of Pure Literal Elimination Rule for Non-Uniform Random (MAX) k-SAT Problem with an Arbitrary Degree Distribution

Oleksii Omelchenko, Andrei A. Bulatov

[AAAI-22] Main Track
Abstract: MAX k-SAT is one of canonical NP-hard problems. Its variation called random MAX k-SAT problem was suggested in order to understand how hard it is to solve instances of the problem on average. The most common random model from which random instances get sampled is the uniform model. However, the uniform model, while useful for studying properties of the space of all k-CNF formulas as a whole, cannot capture all the structural properties we observe in the real-world instances.



Therefore, we propose to use another random model called configuration model, which is able to produce instances with an arbitrary variable's degree distribution. Thus, we may focus and ``probe'' different regions of the space of all k-CNF formulas. There are many questions one may ask about the instances from configuration model, and in this paper we study how effective the pure literal elimination rule (or heuristic) performs when solving random MAX k-SAT instances having an arbitrary but fixed variable's degree distribution.



We provide an equality that depends on the distribution of degrees, solving which one obtains the number of clauses the pure literal elimination rule satisfies. We also show how the distribution of variable degrees changes over time as the heuristic progresses.

Introduction Video

Sessions where this paper appears

  • Poster Session 2

    Fri, February 25 12:45 AM - 2:30 AM (+00:00)
    Blue 4
    Add to Calendar

  • Poster Session 9

    Sun, February 27 8:45 AM - 10:30 AM (+00:00)
    Blue 4
    Add to Calendar

  • Oral Session 9

    Sun, February 27 10:30 AM - 11:45 AM (+00:00)
    Blue 4
    Add to Calendar