  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.
