<p>I am not aware of any collections of 2CNF benchmark instances.</p>

<p>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</p>

<p><a href="https://arxiv.org/abs/1411.1995" rel="noreferrer">https://arxiv.org/abs/1411.1995</a></p>

<p>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 </p>

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

<p>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 <a href="http://www.cril.univ-artois.fr/KC/eadt.html" rel="noreferrer">http://www.cril.univ-artois.fr/KC/eadt.html</a> ) are based on exhaustive DPLL, this should answer your alternative question. </p>

<p>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. </p>

<p>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).</p>

CC BY-SA 3.0
2017-10-10T21:30:01.877Z
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,...)?
delete000
CC BY-SA 3.0
2017-10-10T22:56:11.520Z
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?
delete000
CC BY-SA 3.0
2017-10-11T04:51:43.253Z
@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.
holf
CC BY-SA 3.0
2017-10-09T16:02:00.973Z
2017-10-09T16:02:00.973Z
smengel
<p>Are there any libraries of #2-SAT instances that are hard to solve with state-of-the-art exact solvers (sharpSAT, cachet, ...)?</p>

<p>Alternatively: are there practical ways to generate hard #2-SAT instances?</p>

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

CC BY-SA 3.0
2017-10-07T08:59:40.583Z
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...
holf
<reference-request><sat><counting-complexity><random-k-sat>
How to benchmark #2-SAT counting algorithms?
delete000
# How to benchmark #2-SAT counting algorithms?

(Asked by: username_0 on 2017-10-06)

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$.

**Tags:** reference-request, sat, counting-complexity, random-k-sat
> **Comments:**
> **username_1**: 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...  

---

## 1 answers

### Answer by username_2 on 2017-10-09. Score: 6 | Accepted answer

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).

> **Comments:**
> **username_0**: 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,...)?  
> **username_0**: 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?  
> **username_1**: @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.  

---

