7
$\begingroup$

Are there any libraries of #2-SAT instances that are hard to solve with state-of-the-art exact solvers (sharpSAT, cachet, ...)?

Alternatively: are there practical ways to generate hard #2-SAT instances?

I have only been able to find benchmark instances for #k-SAT for $k\ge3$.

| cite | improve this question | |
$\endgroup$
  • 1
    $\begingroup$ Some vertex cover benchmarks (satisfying assignments of a monotone 2-CNF are in one to one correspondence with the VC of the underlying graph) may be interesting though I do not know if you can compare with existing studies... $\endgroup$ – holf Oct 7 '17 at 8:59
5
$\begingroup$

I am not aware of any collections of 2CNF benchmark instances.

However, one practical way of constructing #2-SAT instances that are provably hard for state-of-the-art model counters is as follows: generate a $d$-regular expander for some constant $d$ (so in practice a random $d$-regular graph), then, as holf suggested, construct the 2CNF-formula that has for every edge $uv$ the clause $x_u\lor x_v$. By this paper

https://arxiv.org/abs/1411.1995

of Bova et al, the resulting formulas do not have small circuits of the form that is called DNNF in knowledge compilation, as subfield of artificial intelligence. Then by connections between DPLL-based model counting and DNNF that can be found in

Huang, Jinbo, and Adnan Darwiche. "DPLL with a trace: From SAT to knowledge compilation." IJCAI. Vol. 5. 2005.

it follows that all DPLL-based model counters will take exponential time to solve the above instances. Since all exact model counters that I am aware of (except for this knowledge compiler that can also used for counting http://www.cril.univ-artois.fr/KC/eadt.html ) are based on exhaustive DPLL, this should answer your alternative question.

Note that the results of Bova et al. are rather asymptotic (there are some small hidden constants in the analysis) but from my experience with similar problems, actual implemented model counters should fail quite early on those instances.

Note that these instances might not be the ones you are looking for: instead of challenging state-of-the-art model counters, they just outright break them provably. So to work around this, you would have to completely change the approach from DPLL to something else similarly to the compiler I linked above (which I don't think will work on these instances, either).

| cite | improve this answer | |
$\endgroup$
  • $\begingroup$ This is helpful. While I wrap my head around this, I have a couple of follow-up questions: when you say "model counters should fail quite early", do you mean the exponential character will be exposed already for small numbers of variables / clauses? If so, do you have an estimate of the order of magnitude (10,100,1000,...)? $\endgroup$ – delete000 Oct 10 '17 at 21:30
  • $\begingroup$ Also, if I understand correctly, the results in Bova et al. hold for $d\ge3$, which corresponds to a ratio of clauses over variables $\alpha=3$ if I choose the graph to be regular. But what about negations? For example, would monotone 2CNF instances generated by this protocol also be hard to count? $\endgroup$ – delete000 Oct 10 '17 at 22:56
  • 1
    $\begingroup$ @delete000: only monotone 2CNF are generated by this. And they are hard to count even for relatively small values of n. I would say n=100 should already be too hard for modern solvers (your graph is random, you might be lucky and find easy graphs ...), maybe less. $\endgroup$ – holf Oct 11 '17 at 4:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.