Engineering – Computer-aided design.

Malay K Ganai, Lintao Zhang, Pranav Ashar, Aarti Gupta, and Sharad Malik1

1

NEC USA CCRL, Princeton NJ 1EE Dept, Princeton University {malay,ashar,agupta}@nec-lab.com {lintaoz,malik}@ee.princeton.edu

Abstract

We propose Satisfiability Checking (SAT) techniques that lead to a consistent performance improvement of up to 3x over state-of-the-art SAT solvers like Chaff on important problem domains in VLSI CAD. We observe that in circuit oriented applications like ATPG and verification, different software engineering techniques are required for the portions of the formula corresponding to learnt clauses compared to the original formula. We demonstrate that by employing the same innovations as in advanced CNF-based SAT solvers, but in a hybrid approach where these two portions of the formula are represented differently and processed separately, it is possible to obtain the consistently highest performing SAT solver for circuit oriented problem domains. We also present controlled experiments to highlight where these gains come from. Once it is established that the hybrid approach is faster, it becomes possible to apply low overhead circuit-based heuristics that would be unavailable in the CNF domain for greater speedup.

Categories and Subject Descriptors

J.6 [Computer Applications]: Computer-aided Engineering – Computer-aided design.

General Terms

Algorithms, Performance, Experimentation,Verification.

Keywords

Boolean Satisfiability (SAT), Boolean Constraint

Propagation (BCP), Conjunctive Normal Form (CNF), Bounded Model Checking (BMC).

1. Introduction

The Boolean Satisfiability (SAT) problem has extensive applications in VLSI CAD. Recent advances in SAT solvers based on Conjunctive Normal Form (CNF) representation have resulted in significantly improved performance. In particular, innovative techniques for decision variable selection [1], Boolean

Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies arenot made or distributed for profit or commercial advantage and that copiesbear this notice and the full citation on the first page. To copy otherwise,or republish, to post on servers or to redistribute to lists, requires prior

specific permission and/or a fee.

DAC 2002, June 10-14, 2002, New Orleans, Louisana, USA. Copyright 2002 ACM 1-58113-461-4/02/0006…$5.00.

1

constraint propagation (BCP) [1, 2], and backtracking with conflict analysis based learning [1, 3] have led to high-performance CNF-based SAT solvers like Chaff [1]. For circuit application domains such as Automatic Test Pattern Generation (ATPG) [4], equivalence checking [5], and Bounded Model Checking (BMC) [6], the Boolean reasoning problem is typically derived from the circuit structure. This has also led to interest in circuit-based SAT solvers [4, 5, 7, 8], which use circuit specific knowledge to guide the search. In general, attempts to include circuit structure information into CNF-based solvers have been unsuccessful due to significant overhead. Furthermore, it is also difficult to integrate CNF-based solvers with other useful techniques like BDD sweeping and dynamic circuit transformation [5]. On the other hand, CNF-based solvers are better than circuit-based solvers in handling conflict analysis and learned clauses [1].

In this paper, we propose techniques that combine the strengths of circuit-based and CNF-based SAT solvers. In particular, we describe a hybrid SAT solver where the original logic formula is processed in circuit form, and the learned clauses are processed separately in CNF. We discuss important differences between the two approaches, and highlight how we reap benefits from both by employing state-of-art innovations in BCP, decision variable selection, and backtracking. Our technique leads to a consistent performance improvement of up to 3x over state-of-the-art SAT solvers like Chaff on representative problem applications.

2. Motivation for Hybrid SAT

Boolean Constraint Propagation (BCP) forms the core of deduction in many successful and widely studied SAT algorithms based on the DPLL algorithm [9]. When a variable is assigned, BCP is used to find the consequences of the assignment, like unit clauses produced and whether a conflict exists. It constitutes about 80% of the total SAT time in our experience. Therefore, any improvement in BCP significantly benefits the overall performance of a SAT solver. We start by describing the details of the circuit-based BCP and CNF-based BCP that we use in our approach. Their relative strengths motivate the specific hybrid scheme we use.

2.1 Circuit-Based BCP

Existing circuit-based SAT solvers [4, 5, 7, 8] use a circuit representation based on AND and OR gate vertices, with INVERTERs either as separate vertices, or as attributes on the gate inputs. Constant propagation across AND/OR gates is, of course, well known, but the speed tends to be very implementation dependent. We use a lookup table for fast implication propagation [5]. Based on the current values of the inputs and output of the vertex, the lookup table determines the

next “state” of the gate where the state encapsulates any implied values and the next action to be taken for the vertex. The algorithm imply (from [5]), shown in Figure 1 for a generic vertex type, iterates over the circuit graph. For each vertex, it determines new implied values and the direction for further processing. As an example, Figure 2 (from [5]) shows some cases from the implication lookup table for a two-input AND gate. For Boolean logic, only one case, a logical 0 at the output of an AND vertex, requires a new case split to be scheduled for justification. All other cases either cause a conflict and backtracking, or further implications, or a return to process the next element to be justified. Due to its low overhead, this implication algorithm is highly efficient. As an indication, on a 750MHz Intel PIII with 2.2 CNF-Based BCP

For CNF, we use the BCP scheme called lazy update proposed by Chaff [1] :

1. For each clause, only two literals are monitored for state

change.

2. The clause state is updated lazily when a variable is

assigned, i.e., only when the two monitored literals coincide. 3. It does not require state change for clauses during the

backtracking process, thus unassigning a variable takes constant time.

For clauses with many literals, lazy update works significantly better than other schemes like SATO [2], and GRASP[3]. It is especially useful for large clauses where it avoids unnecessary 256 MB, it can execute over one million implications per second.

Algorithm imply (vertex, value) { assign (vertex, value);

lvalue = get_value (vertex->left); rvalue = get_value (vertex->right);

next_state = lookup (value, lvalue, rvalue); switch (next_state) { case CONFLICT: return 0;

case CASE_SPLIT:

add_vertex(vertex, justification_queue); return 1; …

case PROP_LEFT_AND_RIGHT:

if (imply (vertex->left, next_state->lvalue) && imply (vertex->right, next_state->rvalue)) { return 1; }

return 0; … }

return 1; }

Figure 1: Circuit-based BCP Procedure

CurrentNextAction11XXXXSTOP00X1X1CONFLICTXXX0X0CASE_SPLIT00XXX0PROP_FORWARDX1X111PROP_LEFT_RIGHT. . .. . .. . .Figure 2: 2-Input AND Lookup Table for Fast Implication Propagation traversal.

2.3 Comparison of BCP Algorithms

There is an inherent overhead built into the translation of circuit gates into clauses. A two-input gate translates to three clauses in the CNF approach, while in the circuit-based approach a gate is regarded as a monolithic entity. Therefore, in the circuit approach an implication across a gate requires a single table lookup, while in the CNF approach it requires processing multiple clauses. In addition, the CNF-based BCP in Chaff does not keep track of the clauses that have been satisfied in order to reduce overheads. However, there is an inherent cost associated with visiting the satisfied clauses. Specifically, even if a clause gets satisfied due to an assignment to some un-watched literal, the watched literal pointers could still get updated. Overall, for the generally small clauses arising from circuit gates, these differences translate to significant differences in BCP time, usually in favor of the circuit-based approach.

On the other hand, learned clauses arising from conflict analysis are typically much larger than those arising from two-input gates. Adding a large learned clause as a gate tree can lead to a significant increase in the size of the circuit. This in turn, can increase the number of implications, thereby negating any potential gains obtained from circuit-based BCP. For such clauses, it is more appropriate to maintain them as monolithic clauses and take advantage of CNF-based 2-literal watching and lazy update to process them efficiently. Based on these observations, we propose a hybrid approach in which we maintain the circuit-based logic expressions using a uniform-gate data structure, and the learned clauses as CNF. We process them separately using the appropriate BCP approach. 2.4 BCP Results Our experimental results for BCP are shown in Table 1. The times shown are in seconds per million implications on a 750 MHz Intel PIII with 256 MB. The examples used are large logic formulas derived from the BMC application on a large industrial circuit. The columns Hybrid and Chaff show BCP times for the hybrid and CNF approaches, respectively, on learned clauses added during SAT as well as the original circuit formula. The size of the formula in terms of the number of primary inputs and gates is indicated in the columns pi and gate. The column CH is the ratio between the Chaff and Hybrid BCP times. It is clear that the hybrid approach is consistently faster than the CNF-based approach in Chaff on these large problems. 2

LogicpigateBCP Time (sec/million implications)FormulaHybridChaffCHStructureCSHS230U50162283461.1541.51.370.91.761.28252U52442421701.1681.5861.350.9141.731.28272U52442387551.1011.4111.280.41.5781.23274S38631792171.111.521.3690.9081.671.22275U54722559791.1621.5661.3470.9551.1.22276U54722560001.1721.5711.340.911.721.29405U66123250691.2361.6051.290.921.741.34406U66123250901.2071.6391.350.941.741.28407U66123250901.2321.6941.3750.9421.7981.31409U66123250901.2451.6391.3160.9231.7751.35435U 6840331.2331.6681.350.9951.6761.242dlx_100 557338481.822.221.210.9312.381.95Table 1: BCP Time per million implications

To demonstrate the effect of learned clauses, we also present the BCP time per million implications for the circuit-based method on only the circuit formula for the same problems, shown in the Column Structure. Note that this is, in a sense, the best case possible, since BCP on the learned clauses is not strictly necessary for the search. Now, the column CS (HS) is the ratio between the Chaff (Hybrid) time and the Structure time, and reflects the overhead due to the extra work in performing BCP on the learned clauses as well. Clearly, large learned clauses introduce a significant overhead in comparison to the circuit formula alone. Our hybrid approach uses the better-suited CNF approach for large learned clauses.

3. Hybrid SAT Solver

A faster BCP with the hybrid approach is only the partial story. The additional benefit of a hybrid approach is that circuit-based decision heuristics can be easily applied, which are otherwise unavailable in a pure CNF approach. Thus, the overall speedup we observe with our hybrid solver can be attributed to the improved BCP in the deduction engine, and additional use of circuit-based heuristics in the decision engine. In this section we demonstrate the benefits derived from them. The diagnosis engine in our hybrid solver is similar to that in Chaff [1], originally proposed by GRASP [3]. In the hybrid approach, conflict driven learning records both clauses and circuit nodes as the reasons for the failure of search.

Our experimental results are presented in Table 2. The times are on a 750 MHz Intel PIII with 256 MB. The logic formulas are derived from the application of BMC on three large industrial circuits (bus, arbiter, and controller) and some public domain benchmarks1 [10] for which circuit descriptions were available. (Note that use of our hybrid approach requires a circuit description, which is not available for most public benchmarks for SAT.) In order not to pollute the results, we ran the hybrid approach on more than 70 logic formulas, but report results only on those requiring more than 40s of CPU time. The formulas are distributed between unsatisfiable and satisfiable instances. The size of the formula can be determined from the pi and gate columns indicating the number of primary inputs and gates.

1

In the table, 2dlx* is 2dlx_cc_mc_ex_bp_f_new

3.1 Comparison of Chaff and Hybrid SAT for

Identical Heuristics

Our first comparison is between the hybrid solver and Chaff for exactly the same heuristics, i.e. without use of any circuit-based decision heuristics. Apart from the different BCP algorithms on the circuit formula, the two use identical algorithms for order of processing of implications, conflict-based learning, backtracking, and decision variable selection. In spite of the same heuristics, a minor difference can creep in due to the uncontrolled choice of the conflict node when several nodes are in conflict. This difference may have a pronounced effect in satisfiable instances, for which one of the two solvers may get lucky in hitting upon a solution early. However, it has relatively less effect in unsatisfiable instances since the entire search space must be explored. With this in mind, we consider only the unsatisfiable instances as reasonable data for this controlled experiment. The columns Chaff and H indicate the times for the Chaff and hybrid solvers, respectively. Due to unavailability of a circuit-based solver in public domain, we could not provide any comparison results with such solvers at this time.

It is clear that the overall performance of the hybrid solver is

much better than Chaff. The typical ratio of Chaff time to H

Examplepi gate ChaffHH-jftC/HC/H-jftUnsatisfiable Instances53U 638454677913.431629.05639.201.162.9655U 66125711851585.081402.80715.201.132.2251U 61565241161283.821010.90508.801.272.5247U 57004770471190.05863.60391.871.383.0449U 59284997101072.738.30606.701.451.77435U 684033922.61326.50317.002.832.913pipe 19810810920.50245.60566.903.751.6245U 54724521888.815.27443.402.142.00434U 684033880.84532.10318.001.662.77407U6612325090736.49367.20588.002.011.25438U 6840337.71427.20283.001.522.29437U 684033621.17281.10419.002.211.48439U 684033599.14441.80453.001.361.32436U 684033559.08369.60384.001.511.46105U 101794528547.68248.90506.302.201.08409U6612325090496.31437.20329.001.141.51406U6612325090486.86353.90317.001.381.54405U6612325069471.50585.00445.000.811.03U 5244429978471.13353.87181.251.332.60109U 1055101180441.33173.70229.002.541.93408U6612325090433.21358.10347.001.211.2541U 501055723.03230.27233.801.581.5639U 4788382909307.59208.87120.201.472.56101U 97988088230.97141.00117.001.1.97276U5472256000193.24132.30104.001.461.8637U 4560358503174.47146.96139.121.191.25252U5244242170165.46118.3093.501.401.7735U 4332335840165.20128.9076.021.282.17275U5472255979162.97132.10129.001.231.26230U5016228346132.54100.6077.001.321.7233U 410431143498.80.1042.101.232.3431U 387628877192.2251.3029.301.803.152dlx* 41425075.0749.3072.401.811.23272U524423875547.5427.708.001.725.94Satisfiable Instances109S 2374144590811.12330.4182.52.454.44105S 2286134654432.22196.472.92.205.93108S 2367142198423.63766.8138.50.553.06101S 2198125070388.35399.38111.90.973.47102S 2235127558344.34312.7144.41.102.38103S 2242129818343.95481.886.70.713.97107S 2330139578286.1256.4178.21.121.61104S 2279132350270.01384.449.10.705.50106S 2323137230226.57198.54.41.142.40100S 2191120305153.41374.7.80.411.572dlx_100 55733848120.1276.8171.567.07Table 2: Comparison of Hybrid SAT Solver and Chaff

3

time, shown in the Column C/H, is greater than 1.3, with the maximum being 3.75. The ratio of the total time spent in Chaff to the total time spent in the hybrid solver for all the unsatisfiable instances is 1.48. Due to possibly a bad choice for a conflict node, we do see a larger time with the hybrid solver in a few cases, e.g., 405U.

For the satisfiable instances shown in Table 2, the Chaff to Hybrid ratio is distributed evenly on either side of 1.0 with a large standard deviation. This is most likely due to the randomness in choice of a conflict node, as explained earlier.

3.2 Incorporation of Circuit-Based Heuristics

Once it is established that the hybrid approach is, in fact, faster, it becomes possible to apply low overhead circuit-based heuristics that would be unavailable in the CNF domain to obtain an even higher speedup. Information regarding gate fanout/fanin, paths, and signal direction becomes readily available without overhead. We find that such an approach works much better than the circuit-oblivious decision heuristics used in the pure CNF-based methods. As an example, the column H-jft in Table 2 shows the time in our hybrid SAT solver with the use of the justification frontier heuristic [7]. This heuristic restricts the decision nodes to be those that justify the values on their fanout node. The use of this heuristic further improves performance in 24 of the 34 unsatisfiable instances. The ratio of the total time spent in Chaff to the total time spent in the hybrid solver for the unsatisfiable instances is now 1. versus the earlier 1.48, with the maximum ratio being 5.94 versus the earlier 3.75.

Now consider the satisfiable instances in Table 2. Where there was wide variation in the speedups (or lack thereof) earlier, we now have consistent and significant speedup over the CNF approach. The ratio of the total time spent in Chaff to the total time spent in the hybrid solver is now 3.24 for the satisfiable instances with the maximum ratio being 7.07. Clearly, the circuit heuristics lead to a satisfying solution much faster than the decision heuristics in Chaff.

Based on these data, there appears to be a clear benefit in using the circuit-based heuristics for both the satisfiable and unsatisfiable instances. In a sense, the hybrid approach allows us to exploit the benefits of the circuit-based as well as the CNF-based heuristics.

3.3 Impact on Verification Applications

SAT is a core engine in many verification applications like equivalence checking [5], and BMC [6]. In fact, it is typical for a long BMC run to last for multiple days, requiring thousands of applications of the SAT solver. A speed up by a factor of two in the core engine, therefore, can prove to be very significant since it would lead to a large absolute saving in the run time. Another practical aspect of our hybrid approach is that it is unnecessary to incur the overhead of copying the entire circuit into a CNF data structure for the purpose of SAT. This has the benefit of reducing the memory requirement of these applications, allowing them to scale to larger circuits, or in the case of BMC, also to a larger number of time frames.

4

4. Conclusions

We have presented a hybrid SAT solver that combines the strengths of circuit-based and CNF-based SAT solvers. We demonstrated it to be the highest performing SAT solver in circuit-based application domains. Our approach is based on an analysis of the source of efficiencies in state-of-art techniques for BCP, decision variable selection, and backtracking. We apply this understanding to develop SAT techniques leveraging off the circuit nature of these application domains while maintaining advantages arising from the CNF representation. Moreover, any future improvements in the performance of circuit-based and CNF-based SAT solvers can directly translate into improvements of the hybrid SAT solver as well.

References

[1] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S.

Malik, \"Chaff: Engineering an Efficient SAT Solver,\" in Proceedings of Design Automation Conference, 2001. [2] H. Zhang, \"SATO: An efficient propositional prover,\" in

Proceedings of International Conference on Automated Deduction, vol. 1249, LNAI, 1997, pp. 272-275.

[3] J. P. Marques-Silva and K. A. Sakallah, \"GRASP: A Search

Algorithm for Propositional Satisfiability,\" IEEE

Transactions on Computers, vol. 48, pp. 506-521, 1999. [4] M. Schulz, E. Trischler, and T. Sarfert, \"SOCRATES: A

highly efficient ATPG System,\" IEEE Transactions on

Computer-Aided Design of Integrated Circuits and Systems, vol. 7, pp. 126-137, 1988.

[5] A. Kuehlmann, M. Ganai, and V. Paruthi, \"Circuit-based

Boolean Reasoning,\" in Proceedings of Design Automation Conference, 2001.

[6] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu, \"Symbolic

Model Checking without BDDs,\" in Proceedings of Workshop on Tools and Algorithms for Analysis and

Construction of Systems (TACAS), vol. 1579, LNCS, 1999. [7] H. Fujiwara and T. Shimono, \"On the Acceleration of Test

Generation Algorithms,\" IEEE Transactions on Computers, vol. C-32, pp. 265-272, 1983.

[8] P. Goel, \"An implicit enumeration algorithm to generate

tests for Combinational circuits,\" IEEE Transactions on Computers, vol. C-30, pp. 215-222, 1981.

[9] M. Davis, G. Longeman, and D. Loveland, \"A Machine

Program for Theorem Proving,\" Communications of the ACM, vol. 5, pp. 394-397, 1962. [10] M. N. Velev, \"Benchmark Suites.

http://www.ece.cmu.edu/~mvelev,\" October 2000.