Finding all Solutions to a CNF. The DualSat SAT Solver

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

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.