English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

In this paper we investigate how to estimate the hardness of Booleansatisfiability (SAT) encodings for the Logical Equivalence Checking problem(LEC). Meaningful estimates of hardness are important in cases when aconventional SAT solver cannot solve a SAT instance in a reasonable time. Weshow that the hardness of SAT encodings for LEC instances can be estimated\textit{w.r.t.} some SAT partitioning. We also demonstrate the dependence ofthe accuracy of the resulting estimates on the probabilistic characteristics ofa specially defined random variable associated with the consideredpartitioning. The paper proposes several methods for constructingpartitionings, which, when used in practice, allow one to estimate the hardnessof SAT encodings for LEC with good accuracy. In the experimental part wepropose a class of scalable LEC tests that give extremely complex instanceswith a relatively small input size $n$ of the considered circuits. For example,for $n = 40$, none of the state-of-the-art SAT solvers can cope with theconsidered tests in a reasonable time. However, these tests can be solved inparallel using the proposed partitioning methods.

Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits