DualSAT is a performant new SAT-solver that is optimized to find and output all solutions to an input CNF usable by further processing steps that can follow. Solutions are stored as a number of disjoint solution classes that happen to be in Decomposable Negation Normal Form (DNNF).
The solver implements new features like unentangled literal detection and backtracking with stack redo. Unentangled literal detection detects the remaining CNF to be in DNNF while a stack redo saves valuable work on conflict directed backjumps because much of the solver's stack content remains preserved. A combination of conflict dependent and independent heuristics ensures good results for known as well as novel and random CNFs. The dual data structures of DualSAT may also prove beneficial for new techniques with enhanced reasoning.
Inhaltsverzeichnis (Table of Contents)
- Introduction
- The Idea about DualSat
- SAT-Solver Technology
- Preliminaries
- Encoding a Problem as SAT
- Resolution, Preprocessing
- DPLL Solvers
- DPLL with Chronological Backtracking
- Clause Learning
- DPLL with Conflict Directed Backjumping
- DPLL with Stack Redo
- Practical Examples for the Stack Redo
- DNNF, Extended Solution Classes and Other Known Algorithms for SAT-Solving
- Efficient Data Structures for SAT-Solvers
- Literal Counting
- Watched Literals and Lazy Data Structures
- The Data Structures of DualSat
- DualSat
- Unentangled Literal Detection
- The Variable Selection Heuristic of DualSat
- Some Other Implementation Details of DualSat
- Wide Integer Implementation for DualSat
- Interesting #SAT solvers
- Clasp and Nogoods in DualSat
- sharpSAT and Component Caching
- Conclusion and Outlook
- Benchmarks
- rutgers.edu DualSat
- rutgers.edu Clasp
- rutgers.edu sharpSAT
- rutgers.edu one solution DualSat
- rutgers.edu one solution Clasp
- rutgers.edu one solution ZChaff
- DQMR DualSat
- Epilogue
- List of References
Zielsetzung und Themenschwerpunkte (Objectives and Key Themes)
This Master's Thesis focuses on the development of a SAT solver called DualSat, aiming to find all solutions to a given problem. It contrasts with traditional SAT solvers that return only a single solution. The thesis explores efficient data structures and algorithms for solving #SAT problems, which involve counting the number of solutions to a propositional formula. Key themes include:- Efficient algorithms for finding all solutions to a CNF (Conjunctive Normal Form) formula.
- The development and implementation of DualSat, a novel SAT solver with a dual data structure approach.
- Comparison of DualSat's performance against established SAT solvers like ZChaff and Clasp.
- Exploration of extended solution classes and the concept of DNNF (Decomposable Negation Normal Form).
- The importance of #SAT problems in various fields, including optimization, planning, and probabilistic reasoning.
Zusammenfassung der Kapitel (Chapter Summaries)
- Introduction: The chapter introduces the concept of SAT solving, emphasizing the shift from finding a single solution to the need for finding all solutions. It highlights the importance of #SAT in solving real-world problems like verification and optimization. The chapter also introduces the idea behind DualSat and its goal to return solution classes as compactly as possible.
- SAT-Solver Technology: This chapter provides a comprehensive overview of SAT-solver technology. It covers essential concepts like encoding a problem as SAT, resolution, preprocessing, and different DPLL solver variants, including Chronological Backtracking, Clause Learning, Conflict Directed Backjumping, and Stack Redo. The chapter also discusses efficient data structures, including literal counting, watched literals, and lazy data structures.
- DualSat: This chapter delves into the details of DualSat, the novel SAT solver developed in this thesis. It explains the core principles of DualSat, including unentangled literal detection, the variable selection heuristic, implementation details, and its wide integer implementation.
- Interesting #SAT Solvers: This chapter explores other notable #SAT solvers, focusing on Clasp and its use of nogoods, and sharpSAT and its approach to component caching.
- Benchmarks: The chapter presents the results of benchmark tests comparing DualSat's performance against other SAT solvers like ZChaff and Clasp. It highlights the strengths and weaknesses of DualSat in finding both single and multiple solutions.
Schlüsselwörter (Keywords)
This Master's Thesis centers around the development and evaluation of a novel SAT solver, DualSat. The key keywords include: SAT solver, #SAT, solution counting, model counting, DualSat, unentangled literal detection, conflict dependent and independent heuristic, backtracking with stack redo, dual data structures, DNNF, extended solution classes, benchmark analysis. The thesis also explores the efficiency and practical application of SAT solving techniques in various fields, including optimization, verification, and planning.
Final del extracto de 66 páginas
- subir
- Citar trabajo
- Elmar Stellnberger (Autor), 2020, Finding all Solutions to a CNF. The DualSat SAT Solver, Múnich, GRIN Verlag, https://www.grin.com/document/1022264
Leer eBook
