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.
Table of Contents
1 Introduction
1.1 The Idea about DualSat
2 SAT-Solver Technology
2.1 Preliminaries
2.1.1 Encoding a Problem as SAT
2.1.2 Resolution, Preprocessing
2.2 DPLL Solvers
2.2.1 DPLL with Chronological Backtracking
2.2.2 Clause Learning
2.2.3 DPLL with Conflict Directed Backjumping
2.2.4 DPLL with Stack Redo
2.2.4.1 Practical Examples for the Stack Redo
2.3 DNNF, Extended Solution Classes and Other Known Algorithms for SAT-Solving
2.4 Efficient Data Structures for SAT-Solvers
2.4.1 Literal Counting
2.4.2 Watched Literals and Lazy Data Structures
2.4.3 The Data Structures of DualSat
2.5 DualSat
2.5.1 Unentangled Literal Detection
2.5.2 The Variable Selection Heuristic of DualSat
2.5.3 Some Other Implementation Details of DualSat
2.5.4 Wide Integer Implementation for DualSat
2.6 Interesting #SAT solvers
2.6.1 Clasp and Nogoods in DualSat
2.6.2 sharpSAT and Component Caching
3 Conclusion and Outlook
4 Benchmarks
4.1 rutgers.edu DualSat
4.2 rutgers.edu Clasp
4.3 rutgers.edu sharpSAT
4.4 rutgers.edu one solution DualSat
4.5 rutgers.edu one solution Clasp
4.6 rutgers.edu one solution ZChaff
4.7 DQMR DualSat
Epilogue
Research Objectives and Core Themes
The primary objective of this thesis is the development and implementation of DualSat, a SAT solver specifically designed to enumerate all solutions to a given propositional formula, rather than just returning a single satisfying assignment. The work explores advanced data structures, conflict-directed backjumping, and a novel "stack redo" mechanism to efficiently navigate the search space of Conjunctive Normal Form (CNF) instances.
- Architectural design and implementation of the DualSat SAT solver.
- Development of the "stack redo" algorithm for enhanced backtracking efficiency.
- Implementation of unentangled literal detection to optimize the search process.
- Comparative performance analysis against existing state-of-the-art solvers like Clasp and sharpSAT.
Excerpt from the Book
1.1 The Idea about DualSat
The initial idea about DualSat was to write a solver that returns not just one but all solutions to a given problem. This is different from plain SAT solvers which only return the first solution they can find and actually different from merely counting solutions. This may be important if a problem cannot be expressed solely by SAT as a CNF but if you have a coherent optimization problem on the number of satisfiable instances. That is why DualSat aims to return solution classes that are as compact as possible. One solution class encompasses many solutions on which a postprocessor may f.i. execute a non-linear optimization problem later on. There are plenty of NP-hard problems in computer science and some are linked to not just return any solution but to find the best possible solution of a host of solutions.
A simple solution class defines a zero or one value for a number of variables and leaves some other variables unassigned. You may write such a solution class as 01xx1 which means x1=0, x2=1, x5=1. In deed the very first solvers like CDP did already return such simple solution classes [BHMW08]. However the old style literal counting scheme of this implementation has some time been replaced with lazy data structures and watched literals. These require that all variables become assigned before a solution is detected [LyMS05].
Summary of Chapters
1 Introduction: Provides a comprehensive overview of the progress in SAT solving and motivates the need for solvers that can find all solutions to NP-hard problems.
2 SAT-Solver Technology: Details the fundamental algorithms and theoretical background, including DPLL, clause learning, and the specific architecture of DualSat.
3 Conclusion and Outlook: Evaluates the performance of DualSat against established solvers and suggests future enhancements like hybrid data structures and improved preprocessing.
4 Benchmarks: Presents empirical data and execution results for DualSat and competing solvers across a wide range of test instances.
Epilogue: Contains corrections, errata, and a reflective discussion on the development process and the challenges encountered.
Keywords
SAT-solver, DualSat, DPLL, backtracking, stack redo, clause learning, CNF, model counting, conflict-directed backjumping, propositional logic, search space, solution enumeration, performance benchmarking.
Frequently Asked Questions
What is the core focus of this research?
The work focuses on the development of DualSat, a SAT solver aimed at efficiently finding all solutions for a given CNF formula, addressing the limitations of solvers that only return single solutions.
What are the primary technical contributions of DualSat?
Key contributions include the stack redo algorithm, unentangled literal detection, and the use of dual data structures to improve backtracking and search efficiency.
What is the primary objective of the DualSat solver?
The primary objective is to enable the enumeration of solution classes in a compact format, facilitating further optimization tasks on those sets of solutions.
Which algorithmic approaches are employed in this work?
The solver utilizes modified DPLL algorithms, conflict-directed backjumping, and optimized data structures such as watched literals and literal counters.
How is the performance of DualSat validated?
Performance is validated through extensive benchmarking against established tools like Clasp, ZChaff, and sharpSAT across diverse problem instances.
Which key terminology defines this study?
The work is characterized by terms such as SAT-solving, stack redo, clause learning, and model counting within the context of propositional satisfiability.
How does the "stack redo" feature improve solver performance?
The stack redo feature preserves previous work during backtracking, allowing the solver to re-enter search branches more efficiently without restarting from scratch after encountering conflicts.
What is the significance of "unentangled literal detection" in DualSat?
It allows the solver to identify when variables can be safely determined without needing to explore all branches, significantly speeding up the enumeration of solutions.
- Quote paper
- Elmar Stellnberger (Author), 2020, Finding all Solutions to a CNF. The DualSat SAT Solver, Munich, GRIN Verlag, https://www.grin.com/document/1022264
