Abstract
SAT solvers are often challenged with very hard problems that remain unsolved after hours of CPU time. The research community meets the challenge in two ways: (1) by improving the SAT solver technology, for example, perfecting heuristics for variable ordering, and (2) by inventing new ways of constructing simpler SAT problems, either using domain specific information during the translation from the original problem to CNF, or by applying a more universal CNF simplification procedure after the translation. This paper explores preprocessing of circuit-based SAT problems using recent advances in logic synthesis. Two fast logic synthesis techniques are considered: DAG-aware logic minimization and a novel type of structural technology mapping, which reduces the size of the CNF derived from the circuit. These techniques are experimentally compared to CNF-based preprocessing. The conclusion is that the proposed techniques are complementary to CNF-based preprocessing and speedup SAT solving substantially on industrial examples.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Biere, A.: AIGER (AIGER is a format, library and set of utilities for And-Inverter Graphs (AIGs), http://fmv.jku.at/aiger/
Bjesse, P., Boralv, A.: DAG-Aware Circuit Compression For Formal Verification. In: Proc. ICCAD’04 (2004)
Chen, D., Cong, J.: DAOmap: A Depth-Optimal Area Optimization Mapping Algorithm for FPGA Designs. In: ICCAD, pp. 752–759 (2004)
Drechsler, R.: Using Synthesis Techniques in SAT Solvers. Technical Report, Intitute of Computer Schience, University of Bremen, Bremen, Germany (2004)
Biere, A., Eén, N.: Effective Preprocessing in SAT Through Variable and Clause Elimination. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 61–75. Springer, Heidelberg (2005)
Een, N., Sörensson, N.: Translating Pseudo-Boolean Constraints into SAT. Journal on Satisfiability, Boolean Modelling and Computation (JSAT) 2 (2006)
B.L.S. Group : ABC: A System for Sequential Synthesis and Verification, http://www.eecs.berkeley.edu/~alanmi/abc/
Jackson, P., Sheridan, D.: Clause Form Conversions for Boolean Circuits. In: H. Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, Springer, Heidelberg (2005)
Minato, S.: Fast Generation of Irredundant Sum-Of-Products Forms from Binary Decision Diagrams. In: Proc. SASIMI’92 (1992)
Mishchenko, A., Chatterjee, S., Brayton, R.: DAG-aware AIG rewriting: A fresh look at combinational logic synthesis. In: Proc. DAC’06, pp. 532–536 (2006)
Mishchenko, A., Chatterjee, S., Brayton, R.: Improvements to Technology Mapping for LUT-based FPGAs. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 26(2), 240–253 (2007)
Sinz, C.: SAT-Race 2006 Benchmark Set (2006), http://fmv.jku.at/sat-race-2006/
Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constr. Math. and Math. Logic (1968)
Velev, M.N.: Efficient Translation of Boolean Formulas to CNF in Formal Verification of Microprocessors. In: Proc. of Conf. on Asia South Pacific Design Aut. (ASP-DAC) (2004)
Zarpas, E.: Benchmarking SAT Solvers for Bounded Model Checking. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Een, N., Mishchenko, A., Sörensson, N. (2007). Applying Logic Synthesis for Speeding Up SAT. In: Marques-Silva, J., Sakallah, K.A. (eds) Theory and Applications of Satisfiability Testing – SAT 2007. SAT 2007. Lecture Notes in Computer Science, vol 4501. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72788-0_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-72788-0_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72787-3
Online ISBN: 978-3-540-72788-0
eBook Packages: Computer ScienceComputer Science (R0)