More Web Proxy on the site http://driver.im/

article

BerkMin: A fast and robust Sat-solver

Authors:

Eugene Goldberg,

Yakov NovikovAuthors Info & Claims

Discrete Applied Mathematics, Volume 155, Issue 12

Pages 1549 - 1561

https://doi.org/10.1016/j.dam.2006.10.007

Published: 01 June 2007 Publication History

Abstract

We describe a SAT-solver, BerkMin, that inherits such features of GRASP, SATO, and Chaff as clause recording, fast BCP, restarts, and conflict clause ''aging''. At the same time BerkMin introduces a new decision-making procedure and a new method of clause database management. We experimentally compare BerkMin with Chaff, the leader among resolution-based SAT-solvers. Experiments show that our program is more robust than Chaff being able to solve more instances than Chaff in a reasonable amount of time.

References

[1]

Baptista, L. and Marques-Silva, J.P., The interplay of randomization and learning on real-world instances of satisfiability. In: Proceedings of AAAI Workshop on Leveraging Probability and Uncertainty in Computation,

[2]

Bayardo, R.J.J. and Schrag, R.C., Using CSP look-back techniques to solve real-world SAT instances. In: Proceedings of the 14th National Conference on Artificial Intelligence (AAAI'97), pp. 203-208.

[3]

Ben-Sasson, E., Impagliazzo, R. and Wigderson, A., Near optimal separation of treelike and general resolution. In: Proceedings of SAT-2000: Third Workshop on the Satisfiability Problem, pp. 14-18.

[4]

Biere, A., Cimatti, A., Clarke, E.M., Fujita, M. and Zhu, Y., Symbolic model checking using SAT procedures instead of BDDs. In: Proceedings of the Design Automation Conference, DAC'99,

[5]

Brayton, R.K., Logic Minimization Algorithms for VLSI Synthesis. 1984. Kluwer Academic Publishers, Dordrecht.

[6]

Burch, J. and Singhal, V., Tight integration of combinational verification methods. In: Proceedings of International Conference on Computer-Aided Design,

[7]

Davis, M., Longemann, G. and Loveland, D., A machine program for theorem proving. Commun. ACM. v5. 394-397.

Digital Library

[8]

Dubois, O., Andre, P., Boufkhad, Y. and Carlier, J., SAT versus UNSAT. In: Johnson, Trick, (Eds.), Second DIMACS Series in Discrete Mathematics and Theoretical Computer Science, American Mathematical Society. pp. 415-436.

[9]

J.W. Freeman. Improvements to propositional satisfiability search algorithms, Ph.D. Thesis, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, 1995.

[10]

Goldberg, E. and Novikov, Y., BerkMin: a fast and robust SAT-solver. In: Proceedings of Design, Automation and Test in Europe Conference, pp. 142-149.

[11]

E. Goldberg, Ya. Novikov, Equivalence checking of dissimilar circuits, 12th International Workshop on Logic and Synthesis, Laguna Beach, CA, USA, May 28-30, IWLS-2003.

[12]

Goldberg, E. and Prasad, M., Using Sat for combinational equivalence checking. In: Proceedings of Design, Automation and Test in Europe Conference, pp. 114-121.

[13]

Gomes, C.P., Selman, B. and Kautz, H., Boosting combinational search through randomization. In: Proceedings of AAAI'98,

[14]

H. Hoos, T. Stützle, {http://www.satlib.org/benchm.html}.

[15]

Li, C.M., A constrained-based approach to narrow search for satisfiability. Inform. Process. Lett. v71. 75-80.

[16]

Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L. and Malik, S., Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Design Automation Conference (DAC'01),

[17]

Silva, J.P.M. and Sakallah, K.A., GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. v48. 506-521.

Digital Library

[18]

L. Simon, {http://www.lri.fr/~simon/satex/satex.php3}.

[19]

Stephan, P., Brayton, R. and Sangiovanni-Vencentelli, A., Combinational test generation using satisfiability. IEEE Trans. Comput.-Aided Des. Integrated Circuits Syst. v15. 1167-1176.

Digital Library

[20]

M. Velev, CMU benchmark suite, Available from {http://www.ece.cmu.edu/~mvelev}.

[21]

Zhang, H., SATO: an efficient propositional prover. In: Proceedings of the International Conference on Automated Deduction, pp. 272-275.

[22]

L. Zhang, C.F. Madigan, M.H. Moskewicz, S. Malik, Efficient conflict driven learning in a Boolean satisfiability solver, in: Proceeding of ICCAD 2001, pp. 279-285.

[23]

{http://www.ee.princeton.edu/~chaff/spelt3/chaff2_20010323_spelt3-bin-solaris.tar}.

[24]

{http://www.ee.princeton.edu/~chaff/zchaff/zchaff.2001.2.17.solaris.gz}.

[25]

{http://eigold.tripod.com/BerkMin.html}.

[26]

{http://www.satlive.org/SATCompetition/2003/index.jsp}.

Cited By

Wang WZhang NTian CDuan ZXu ZYu C(2023)Verifying Chips Design at RTL LevelTheoretical Aspects of Software Engineering10.1007/978-3-031-35257-7_9(146-163)Online publication date: 4-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-35257-7_9
Yakopcic CRahman NAtahary TTaha TDouglass SDi Natale GFummi F(2020)Solving constraint satisfaction problems using the loihi spiking neuromorphic processorProceedings of the 23rd Conference on Design, Automation and Test in Europe10.5555/3408352.3408598(1079-1084)Online publication date: 9-Mar-2020
https://dl.acm.org/doi/10.5555/3408352.3408598
Alouneh SAbed SAl Shayeji MMesleh R(2019)A comprehensive study and analysis on SAT-solvers: advances, usages and achievementsArtificial Intelligence Review10.1007/s10462-018-9628-052:4(2575-2601)Online publication date: 1-Dec-2019
https://dl.acm.org/doi/10.1007/s10462-018-9628-0
Show More Cited By

Index Terms

BerkMin: A fast and robust Sat-solver

Recommendations

Backjumping for quantified Boolean logic satisfiability

The implementation of effective reasoning tools for deciding the satisfiability of Quantified Boolean Formulas (QBFs) is an important research issue in Artificial Intelligence. Many decision procedures have been proposed in the last few years, most of ...
BerkMin: A Fast and Robust Sat-Solver
DATE '02: Proceedings of the conference on Design, automation and test in Europe

We describe a SAT-solver, BerkMin, that inherits suchfeatures of GRASP, SATO, and Chaff as clause recording,fast BCP, restarts, and conflict clause "aging". At thesame time BerkMin introduces a new decision makingprocedure and a new method of clause ...
A first polynomial non-clausal class in many-valued logic
Abstract
The relevance of polynomial classes of formulas to deductive efficiency motivated their further research, and currently, a great number of such classes is known. Nevertheless, they have been exclusively sought in the setting of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Discrete Applied Mathematics

Discrete Applied Mathematics Volume 155, Issue 12

June, 2007

128 pages

ISSN:0166-218X

Issue’s Table of Contents

Copyright © Elsevier B.V. © 2006.

Publisher

Elsevier Science Publishers B. V.

Netherlands

Publication History

Published: 01 June 2007

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

19
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Wang WZhang NTian CDuan ZXu ZYu C(2023)Verifying Chips Design at RTL LevelTheoretical Aspects of Software Engineering10.1007/978-3-031-35257-7_9(146-163)Online publication date: 4-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-35257-7_9
Yakopcic CRahman NAtahary TTaha TDouglass SDi Natale GFummi F(2020)Solving constraint satisfaction problems using the loihi spiking neuromorphic processorProceedings of the 23rd Conference on Design, Automation and Test in Europe10.5555/3408352.3408598(1079-1084)Online publication date: 9-Mar-2020
https://dl.acm.org/doi/10.5555/3408352.3408598
Alouneh SAbed SAl Shayeji MMesleh R(2019)A comprehensive study and analysis on SAT-solvers: advances, usages and achievementsArtificial Intelligence Review10.1007/s10462-018-9628-052:4(2575-2601)Online publication date: 1-Dec-2019
https://dl.acm.org/doi/10.1007/s10462-018-9628-0
Liang JGovind HPoupart PCzarnecki KGanesh V(2018)An empirical study of branching heuristics through the lens of global learning rateProceedings of the 27th International Joint Conference on Artificial Intelligence10.5555/3304652.3304758(5319-5323)Online publication date: 13-Jul-2018
https://dl.acm.org/doi/10.5555/3304652.3304758
Xiang YZhou YZheng ZLi M(2018)Configuring Software Product Lines by Combining Many-Objective Optimization and SAT SolversACM Transactions on Software Engineering and Methodology10.1145/317664426:4(1-46)Online publication date: 20-Feb-2018
https://dl.acm.org/doi/10.1145/3176644
Lyu YChen LZhang CQu DMin-Allah NWang Y(2018)An interleaved depth-first search method for the linear optimization problem with disjunctive constraintsJournal of Global Optimization10.1007/s10898-017-0602-170:4(737-756)Online publication date: 1-Apr-2018
https://dl.acm.org/doi/10.1007/s10898-017-0602-1
Osama MGaber LHussein AMahmoud H(2018)An Efficient SAT-Based Test Generation Algorithm with GPU AcceleratorJournal of Electronic Testing: Theory and Applications10.1007/s10836-018-5747-434:5(511-527)Online publication date: 1-Oct-2018
https://dl.acm.org/doi/10.1007/s10836-018-5747-4
Liang JGanesh VPoupart PCzarnecki K(2016)Exponential recency weighted average branching heuristic for SAT solversProceedings of the Thirtieth AAAI Conference on Artificial Intelligence10.5555/3016100.3016385(3434-3440)Online publication date: 12-Feb-2016
https://dl.acm.org/doi/10.5555/3016100.3016385
Varshosaz MKhosravi R(2013)Discrete time Markov chain familiesProceedings of the 17th International Software Product Line Conference co-located workshops10.1145/2499777.2500725(34-41)Online publication date: 26-Aug-2013
https://dl.acm.org/doi/10.1145/2499777.2500725
Alviano MDodaro CFaber WLeone NRicca F(2013)WASPProceedings of the 12th International Conference on Logic Programming and Nonmonotonic Reasoning - Volume 814810.1007/978-3-642-40564-8_6(54-66)Online publication date: 15-Sep-2013
https://dl.acm.org/doi/10.1007/978-3-642-40564-8_6
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Issue’s Table of Contents