Research of Branching Heuristic Strategy for Implied Literal in Shortest Clause for SAT Problem
Author: 
Rong HuAuthors Info & Claims
Pages 46 - 50
Abstract
Branching heuristic strategy plays a very important role in CDCL-based algorithms.In this paper, we propose a new branching heuristic inspired by the new dynamic phase selection policy used to improve Glucose 2.0.As it says, SAT solvers now use a new data structure - observing to text structure. When a clause contains implied literal, it automatically assigns the corresponding value, which can be applied here. Its advantage is the use of the integrity of the SAT solver. The main idea of this strategy is to give priority to the shortest clause, and also to reduce the size of the long clause, making it a shorter clause.
References
[1]
Marques-Silva,J. P. and Sakallah, K.A. 1996. GRASP-A new search algorithm for satisfiability. In Proceedings of the International Conference on Computer-Aided Design.(Nov. 1996), 73--89.
[2]
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L.,and Malik, S.2001. Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference. DAC 2001, ACM, New York, NY, 530--535.
[3]
Goldberg, E., and Novikov, Y.2002. BerkMin: A fast and robust SAT-solver. In: Proceedings of Design Automation and Test in Europe(DATE).Springer Netherlands, 1549--1561.
[4]
Eén, N., and Sörensson, N. 2003. An Extensible SAT-solver. Theory and Applications of Satisfiability Testing. Springer Berlin Heidelberg, 502--518.
[5]
Zhang, H. 1997. SATO: An efficient prepositional prover. International Conference on Automated Deduction. Springer-Verlag, 272--275.
[6]
Bayardo, R., and Schrag, R. 1996. Using CSP look-back techniques to solve real-world SAT instance. International Conference on Principles and Practice of Constraint Programming, Cambridge, Massachusetts, Usa, August. DBLP, 46--60.
[7]
Marques-Silva, J. 1999. The impact of branching heuristics in propositional satisfiability algorithms. In: Barahona, P., Alferes, J.J. (eds.) EPIA 1999. LNCS (LNAI), vol.1695, Springer, Heidelberg, 62--74.
[8]
Informatik, R., Buro, M., and Buning, H. K. 2002. Report on a sat competition. Technical report,University of Paderborn.
[9]
Dubois, O., Andre, P., Boufkhad, Y., and Carlier, J. 1996. SAT versus UNSAT. In D. S.Johnson and M. A. Trick, editors, Second DIMACS Implementation Challenge. American Mathematical Society.
[10]
Freeman, J. W. 1996. Improvements to Propositional Satisfiability Search Algorithms.PhD thesis, University of Pennsylvania, Philadelphia, PA.
[11]
Pretolani, D. 1995. Efficiency and stability of hypergraph sat algorithms. In D. S.Johnson and M. A. Trick, editors, Second DIMACS Implementation Challenge.American Mathematical Society.
[12]
Zabih, R., and Mcallester, D. 1988.A rearrangement search strategy for determining propositional satisfiability. In Proceedings of the National Conference on Artificial Intelligence, 155--160.
[13]
Stadtwald, I., and Barth, P. 1995. A Davis-Putnam enumeration procedure for linear pseudo-boolean optimization. Technical Report MPI-I-2-003, MPI.
[14]
Hooker, J. N., and Vinay, V. 1995. Branching rules for satisfiability. Journal of Automated Reasoning, 15:359--383.
[15]
Biere, A.2008.Adaptive restart strategies for conflict driven SAT solvers. In Büning,H.K., Zhao, X., eds.: Theory and Applications of Satisfiability Testing - SAT 2008,11th International Conference, SAT 2008, Guangzhou, China, May 12-15. Proceedings. Volume 4996 of Lecture Notes in Computer Science., Springer, 28--33.
[16]
Ryan, L. 2004. Efficient algorithms for clause-learning SAT solvers. Master's thesis,Simon Fraser University.
[17]
Biere, A., and Frohlich, A. 2015. Evaluating CDCL variable scoring schemes. In Theory and Applications of Satisfiability Testing--SAT 2015. Springer International Publishing. 405--422.
[18]
Chen, J. C. 2012. A Dynamic Phase Selection Strategy for Satisfiability Solvers.DOI=http://arxiv.org/abs/1208.1613.
[19]
Guo, Y., Zhang, C.S., and Zhang, B. 2016. Research progress on Algorithms for solving SAT problems. computer science, 8--17.
[20]
Zhao, S. Y. 2008. Solving SAT problem based on Clause weight. Fudan University.
Index Terms
- Research of Branching Heuristic Strategy for Implied Literal in Shortest Clause for SAT Problem
Recommendations
Clause elimination for SAT and QSAT
The famous archetypical NP-complete problem of Boolean satisfiability (SAT) and its PSPACE-complete generalization of quantified Boolean satisfiability (QSAT) have become central declarative programming paradigms through which real-world instances of ...
Limitations of restricted branching in clause learning
The techniques for making decisions, that is, branching, play a central role in complete methods for solving structured instances of constraint satisfaction problems (CSPs). In this work we consider branching heuristics in the context of propositional ...
A clause-based heuristic for SAT solvers
SAT'05: Proceedings of the 8th international conference on Theory and Applications of Satisfiability TestingWe propose a new decision heuristic for DPLL-based propositional SAT solvers. Its essence is that both the initial and the conflict clauses are arranged in a list and the next decision variable is chosen from the top-most unsatisfied clause. Various ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
June 2017
108 pages
ISBN:9781450352321
DOI:10.1145/3094243
Copyright © 2017 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
In-Cooperation
- Southwest Jiaotong University
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 02 June 2017
Check for updates
Author Tags
Qualifiers
- Research-article
- Research
- Refereed limited
Conference
ICDLT '17
ICDLT '17: 2017 International Conference on Deep Learning Technologies
June 2 - 4, 2017
Chengdu, China
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 62Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 07 Mar 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in