Estimating Satisfiability

TL;DR

This paper introduces a general weighting scheme for estimating the satisfiability of CSPs, improving bounds on non-trivial cores in 3-SAT and comparing it with ordering methods.

Contribution

It proposes a new weighting framework for satisfiability estimation and demonstrates its advantages over existing bounds and methods.

Findings

Improves upper bound on non-trivial cores in 3-SAT to 4.419.

Provides sufficient conditions for correct weighting schemes.

Compares weighting and ordering methods under various conditions.

Abstract

The problem of estimating the proportion of satisfiable instances of a given CSP (constraint satisfaction problem) can be tackled through weighting. It consists in putting onto each solution a non-negative real value based on its neighborhood in a way that the total weight is at least 1 for each satisfiable instance. We define in this paper a general weighting scheme for the estimation of satisfiability of general CSPs. First we give some sufficient conditions for a weighting system to be correct. Then we show that this scheme allows for an improvement on the upper bound on the existence of non-trivial cores in 3-SAT obtained by Maneva and Sinclair (2008) to 4.419. Another more common way of estimating satisfiability is ordering. This consists in putting a total order on the domain, which induces an orientation between neighboring solutions in a way that prevents circuits from appearing, and then counting only minimal elements. We compare ordering and weighting under various conditions.