Electrical Engineering

Abstract

Referring to the proposed approaches from the existing Satisfiability (SAT) solver algorithms, which are based on tree structured searching strategy combining with heuristic approaches to reduce the search space, we treat SAT problems as a logical optimization issue which can be solved by a logic minimizer tool. In this experiment, one of the well-known logic minimizers, ESPRESSO, has been used to minimize the given Boolean functions. In this paper, the partitioning method is proposed which greatly increased the efficiency of ESPRESSO. The proposed method reduces the terms optimized in ESPRESSO by partitioning the given SAT constraints into small groups. From experimental results, the partitioning method can achieve a remarkable performance. (Satoshi et. al 2003)

Electrical Engineering

1. Introduction

Satisfiability (SAT) problem is known as a NP-complete problem with a definition of determining the existed variables assignment denoted by {x1,…,xn}for a Boolean function, F , that can satisfy (F equals to 1) with the given constraints (clauses) or determining there are no such variables existed called Unsatisfied (UNSAT). Over the past decades, SAT problem has been well studied and many SAT solvers have been broadly used as tools inside many different areas of applications including logic synthesis, ATPG, model checking, and equivalence checking. Most existing algorithms are based on tree structured searching algorithm in the similar way as used in DPLL's algorithm.

DPLL is a refinement of Davis-Putnam procedure, by adding a number of enhancements observed from the derivable Boolean equations. Many SAT algorithms (GRASP), SATO, Chaff, and BerkMin have been proposed since DPLL algorithm. However, these solvers still rely exclusively on DPLL algorithm which is considered as a tree structure searching strategy. (Frolund. 2003) For testing the efficiency between the order of clause from the original problems and proposed algorithm, we randomize the clause order of original problems and run the partitioning methods again.

When clause order is randomized, the partitioning method cannot solve any problem within time limit. By applying clauses reordering method and partitioning method, many instances can be solved within time limit. However, if we apply reorder method on the original problem, the computation time is larger than the result without applying reordering method. Therefore, we can conclude the clause order of original problem is in good clauses order. From the experimental results, if the problems are in good clause order, our proposed method can achieve remarkable performance.

This paper proposes the novel partitioning method to solve SAT problems instead of the commonly used tree structured searching algorithm. The algorithms of SAT solver we proposed, utilize a state-of-the-art minimization tool.

A Boolean function can be represented in two forms; Sum-of-Product (SOP) and Product-of-Sum (POS). Boolean variables are denoted by {x1,…,xn} which can be assigned in two values as logic 0 or FALSE, and logic 1 or TRUE. In this paper, a “+” sign is denoted as logic “OR” or “ ”, and a “·” sign is denoted as logic “AND” or “ ”.

Each bracket in (2) is represented as one clause in our input file or being known as Conjunctive Normal Form ...