Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits Alexander Semenov Konstantin Chukharev

2025-04-29 0 0 683.81KB 20 页 10玖币

侵权投诉

Estimating the hardness of SAT encodings for

Logical Equivalence Checking of Boolean circuits

Alexander Semenov* Konstantin Chukharev

Egor Tarasov Daniil Chivilikhin

Viktor Kondratiev

ITMO University, St. Petersburg, Russia

alex.a.semenov@itmo.ru

October 5, 2022

Abstract

In this paper we investigate how to estimate the hardness of Boolean

satisﬁability (SAT) encodings for the Logical Equivalence Checking prob-

lem (LEC). Meaningful estimates of hardness are important in cases when

a conventional SAT solver cannot solve a SAT instance in a reasonable

time. We show that the hardness of SAT encodings for LEC instances

can be estimated w.r.t. some SAT partitioning. We also demonstrate

the dependence of the accuracy of the resulting estimates on the prob-

abilistic characteristics of a specially deﬁned random variable associated

with the considered partitioning. The paper proposes several methods for

constructing partitionings, which, when used in practice, allow one to es-

timate the hardness of SAT encodings for LEC with good accuracy. In

the experimental part we propose a class of scalable LEC tests that give

extremely complex instances with a relatively small input size 𝑛of the

considered circuits. For example, for 𝑛= 40, none of the state-of-the-art

SAT solvers can cope with the considered tests in a reasonable time. How-

ever, these tests can be solved in parallel using the proposed partitioning

methods.

1 Introduction

Boolean circuits are widely used in theoretical computer science [1, 18] as well

as in numerous industrial applications. It would take too much space to list all

the key references regarding the various practical applications of Boolean cir-

cuits. We only note that each hardware implementation of an arbitrary discrete

function (i.e. function 𝑓:{0,1}𝑛→ {0,1}𝑚) can be viewed as some Boolean cir-

cuit, entailing the development of such a colossal industry as Electronic Design

Automation (EDA).

arXiv:2210.01484v1 [cs.AI] 4 Oct 2022

One of the main problems related to Boolean circuits is the logical equiva-

lence checking problem (LEC) [24, 28]. This problem is posed as follows: there

are two circuits 𝑆𝑓, 𝑆ℎspecifying some functions 𝑓, ℎ :{0,1}𝑛→ {0,1}𝑚. The

question is: “Is it true that 𝑓and ℎare equal, i.e. point-wise equality 𝑓∼

=ℎ

holds?”. At the initial stage of development of formal veriﬁcation methods, Bi-

nary Decision Diagrams (BDD) [9] were used to solve LEC. Works [4, 5] argued

in favor of solving LEC via applying complete SAT solvers based on the CDCL

algorithm [25]; currently, LEC is mainly solved with such algorithms: a good

example is the ABC [8] framework.

SAT solvers work with Boolean formulas in Conjunctive Normal Form

(CNF). There is an algorithm linear in the size of circuits 𝑆𝑓, 𝑆ℎthat reduces

LEC for these circuits to SAT for a CNF formula using Tseytin transforma-

tions [34].

Unfortunately, SAT for a CNF formula which encodes LEC for 𝑆𝑓and 𝑆ℎ

can be diﬃcult for state-of-the-art SAT solvers. If we use a sequential solver, in

many cases we cannot even say how much time can be required for solving the

corresponding SAT instance. Prediction of runtime for modern SAT solvers is

very diﬃcult in the general case due to their heavy-tailed behavior [19].

The main goal of this paper is to show that the hardness of a SAT instance

which encodes some LEC problem can be estimated by decomposing this in-

stance into a family of simpler SAT instances. In this context we introduce the

notion of hardness of formula w.r.t. some SAT partitioning. We show that this

hardness measure can be expressed via an expected value of a special random

variable which is associated with a considered SAT partitioning. To estimate

this measure we use the Monte Carlo method. The main issue of this approach

is that the corresponding Monte Carlo estimation can be not accurate enough.

We study the problem how to construct a partitioning of a CNF formula encod-

ing some LEC problem, which gives a hardness estimation of this formula with

high accuracy. We propose two partitioning construction methods which rely on

the structure of considered circuits and justify the good properties of proposed

construction methods in application to extremely hard LEC instances. In par-

ticular, using a computing cluster we solved the LEC instance which turned to

be too hard for sequential SAT solvers which won the SAT Competitions of the

last years.

2 Preliminaries

In this section, we introduce the necessary formal concepts and notation.

2.1 Satisﬁability and Boolean circuits

We start from basic concepts related to SAT, the Boolean Satisﬁability prob-

lem [7]. In the context of SAT one usually works with a Boolean formula in

CNF.

Let 𝐶be an arbitrary CNF formula and 𝑋be the set of Boolean variables

occurring in 𝐶. An assignment of variables from 𝑋is a mapping 𝛼:𝑋→ {0,1}.

The set of all diﬀerent assignments of variables from 𝑋is denoted as {0,1}|𝑋|

and called Boolean hypercube of dimension 𝑛,𝑛=|𝑋|.

In the context of SAT, for an arbitrary CNF formula 𝐶it is required to an-

swer the following question: is it true that 𝐶is satisﬁable? That is, is there

as assignment of variables from 𝑋for which 𝐶is evaluated to true? In this

formulation, SAT is NP-complete, and it is NP-hard when one has to detect

the satisﬁability of 𝐶and, in the case of a positive answer, to ﬁnd some sat-

isfying assignment. Despite the theoretical hardness of SAT, the last 20 years

demonstrate impressive progress in the development of SAT solving algorithms

with a wide spectrum of practical applications in symbolic veriﬁcation, com-

putational combinatorics, bioinformatics, cryptanalysis, etc. One of the most

striking examples is hardware veriﬁcation and, in particular, Logical Equiva-

lence Checking (LEC). As it was said above, in LEC one has to answer the

following question: is it true that two Boolean circuits are equivalent?

As in the majority of related articles, we regard a Boolean circuit as some di-

rected acyclic graph. Consequently, we use the following standard graph theory

deﬁnitions. A (directed) graph 𝐺= (𝑉, 𝐸)consists of a set of vertices 𝑉and a

set of (directed) edges 𝐸⊆𝑉2. An edge is a pair of connected vertices. An arc

is a directed edge, i.e. an ordered pair of vertices. For each arc (𝑢, 𝑣)∈𝐸, ver-

tex 𝑢is called a parent of 𝑣, and 𝑣is called a child of 𝑢. The set of all parents

of a vertex 𝑣is denoted by 𝑃𝑣. The indegree of a vertex 𝑣is the number of

parents of 𝑣, and the outdegree is the number of children. A vertex is called an

input if it has no parents, and an output if it has no children. The sets of inputs

and outputs are denoted as 𝑉𝑖𝑛 ⊂𝑉and 𝑉𝑜𝑢𝑡 ⊂𝑉respectively. A path is a

sequence of arcs. A vertex 𝑢is called a predecessor of 𝑣if there is a path from

𝑢to 𝑣. A predecessor 𝑢which is also an input (𝑢∈𝑉in) is called an ancestor

of 𝑣. The set of all ancestors of a vertex 𝑣is denoted by 𝐴𝑣(ancestor set).

A Boolean circuit with 𝑛inputs and 𝑚outputs can be viewed as a natural

way of specifying some discrete function 𝑓:{0,1}𝑛→ {0,1}𝑚. Implying this,

we will denote an arbitrary Boolean circuit deﬁning a discrete function 𝑓as

𝑆𝑓= (𝑉, 𝐸).

Let 𝑆𝑓be an arbitrary Boolean circuit. Any vertex 𝑣∈𝑉∖𝑉𝑖𝑛 is called

agate. Each gate is associated with some logical connective from a predeﬁned

set called a basis (for example it can be {∧,¬},{∧,∨,¬},{∧,⊕,1}, etc.). An

example of a graphical representation of a Boolean circuit with |𝑉𝑖𝑛|= 3 inputs

and |𝑉∖𝑉𝑖𝑛|= 8 gates is shown in Fig. 1.

The set of vertices 𝑉of a circuit 𝑆𝑓can be naturally partitioned into subsets

called “layers”, which are deﬁned inductively as follows.

Deﬁnition 1 (Circuit layers).Let 𝑉0=𝑉𝑖𝑛 denote the zeroth circuit layer. The

𝑘-th (𝑘≥1) circuit layer 𝑉𝑘is deﬁned inductively as the set of all vertices 𝑣

satisfying the following two properties:

1. 𝑣 /∈𝑘−1

𝑗=0 𝑉𝑗;

𝑖1𝑖2𝑖3

¬∧⊕

∨ ∧

∧ ∧

⊕

Figure 1: An example Boolean circuit with three inputs (𝑖1,𝑖2,𝑖3) and eight

gates

2. 𝑃𝑣⊆𝑘−1

𝑗=0 𝑉𝑗.

Deﬁnition 2 (Associated functions).With each gate 𝑣∈𝑉∖𝑉𝑖𝑛 let us asso-

ciate a predeﬁned Boolean function 𝑔𝑣:{0,1}|𝑃𝑣|→ {0,1}. The value of 𝑔𝑣is

uniquely determined by the values of the functions 𝑔𝑤(𝑤∈𝑃𝑣) with respect to

the semantics of the logical connective which is associated with gate 𝑣.

Let us ﬁx some order on set 𝑉𝑖𝑛 and the same order will apply to the bits of

an arbitrary word from {0,1}𝑛. Thus, each bit of an arbitrary word 𝛼∈ {0,1}𝑛

is uniquely connected with some vertex from 𝑉𝑖𝑛. Let us say that 𝛼is an input

word of 𝑆𝑓.

Deﬁnition 3 (Circuit interpretation).Let 𝛼∈ {0,1}𝑛be an arbitrary in-

put word of the circuit 𝑆𝑓. Begin traversing the circuit starting from the ﬁrst

layer 𝑉1. For any 𝑣∈𝑉1we suppose that the value of an arbitrary 𝑔𝑤(𝑤∈𝑃𝑣,

𝑃𝑣⊆𝑉𝑖𝑛) is equal to the corresponding bit of 𝛼associated with 𝑤. For an ar-

bitrary gate 𝑣∈𝑉𝑗,𝑗 > 1, let us calculate the value of 𝑔𝑣on 𝛼using known

values of 𝑔𝑤on this input word for all 𝑤∈𝑃𝑣. We will also say that this value

of 𝑔𝑣is induced by 𝛼. Continue the evaluation until the values of functions 𝑔𝑣

are calculated for all gates of circuit 𝑆𝑓. Let us call the described process the

interpretation of the circuit 𝑆𝑓on input word 𝛼.

Let 𝑆𝑓be a Boolean circuit with 𝑛inputs and 𝑚outputs. Note that the

interpretation of 𝑆𝑓speciﬁes a total function 𝑓:{0,1}𝑛→ {0,1}𝑚. The value

of this function on an arbitrary word 𝛼∈ {0,1}𝑛is a Boolean vector 𝛾=

(𝛾1, . . . , 𝛾𝑚), where 𝛾𝑘,𝑘∈ {1, . . . , 𝑚}, are the values of functions 𝑔𝑣induced

by 𝛼for all 𝑣∈𝑉𝑜𝑢𝑡.

Deﬁnition 4 (Associated variables).Let us associate with each vertex of circuit

𝑆𝑓a particular Boolean variable and denote the set of all such variables as 𝑋.

Let 𝑋𝑖𝑛 be the set of Boolean variables associated with the inputs of 𝑆𝑓; we will

refer to these variables as to input variables. The variables assigned to gates

文档加载中……请稍候！
如果长时间未打开，您也可以点击刷新试试。

下载文档到电脑，查找使用更方便

10 玖币 0人已下载

立即下载

摘要：

EstimatingthehardnessofSATencodingsforLogicalEquivalenceCheckingofBooleancircuitsAlexanderSemenov*KonstantinChukharevEgorTarasovDaniilChivilikhinViktorKondratievITMOUniversity,St.Petersburg,Russiaalex.a.semenov@itmo.ruOctober5,2022AbstractInthispaperweinvestigatehowtoestimatethehardnessofBooleansati...

展开>> 收起<<

Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits Alexander Semenov Konstantin Chukharev.pdf

共20页,预览4页

还剩页未读，继续阅读

声明：本站为文档C2C交易模式，即用户上传的文档直接被用户下载，本站只是中间服务平台，本站所有文档下载所得的收益归上传人(含作者)所有。玖贝云文库仅提供信息存储空间，仅对用户上传内容的表现方式做保护处理，对上载内容本身不做任何修改或编辑。若文档所含内容侵犯了您的版权或隐私，请立即通知玖贝云文库，我们立即给予删除！

Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits Alexander Semenov Konstantin Chukharev

相关推荐

开通VIP享超值会员特权

作者详情

相关内容

热门标签

举报选择: