SATzillaX is a high-performance Conflict-Driven Clause Learning (CDCL) Boolean Satisfiability (SAT) solver written in pure C++17. Designed to be lightweight, clean, and highly efficient, SATzillaX implements the industry-standard algorithms and heuristics found in modern industrial SAT solvers (like Minisat and Chaff) from scratch.
Boolean Satisfiability is an NP-complete problem, making it a foundation of computer science. SATzillaX tackles hard combinatorial and industrial formulas by utilizing dynamic clause learning, non-chronological backtracking, and variable activity scoring.
- Conflict-Driven Clause Learning (CDCL): Learns new clauses from conflicts to avoid exploring the same unsatisfiable search spaces again.
- 1st UIP (Unique Implication Point) Analysis: Infers optimal conflict clauses by analyzing the implication graph.
- Two-Watched Literals (2WL): Efficient boolean constraint propagation (BCP) that tracks only two literals per clause, reducing overhead significantly during search.
- Non-Chronological Backtracking (Backjumping): Backtracks multiple decision levels at once based on conflict analysis, rather than backtracking step-by-step.
- VSIDS (Variable State Independent Decaying Sum): A dynamic decision branching heuristic using a binary heap (
VarOrderHeap) to focus on variables involved in recent conflicts. - Phase Saving: Saves the last assigned truth value of a variable to guide future decisions.
- Geometric Restarts: Automatically resets the search tree periodically to escape local minima in the search space, while maintaining learned clauses and VSIDS activities.
- Robust DIMACS Parser: Token-based parser handling comments, extra whitespace, and missing problem lines gracefully.
SATzillaX/
├── src/
│ ├── main.cpp # Entrypoint parsing arguments and invoking the solver
│ ├── parser.h # DIMACS parser interface and data structures
│ ├── parser.cpp # Robust token-based CNF parser implementation
│ ├── solver.h # SATSolver class declaration, structures, and helper classes
│ └── solver.cpp # CDCL search, unit propagation, conflict analysis, and VSIDS
├── Makefile # Build automation script
├── .gitignore # Git ignore file for compiled/temporary artifacts
└── README.md # Project documentation (this file)
You need a C++ compiler supporting the C++17 standard (like GCC/g++ 7+, Clang 5+, or MSVC 2017+).
To compile the project with -O0 performance optimization, run:
g++ -std=c++17 -g -O0 src/main.cpp src/parser.cpp src/solver.cpp -o SATzillaXIf you have make installed:
makeTo clean build files:
make cleanSATzillaX accepts input files in the standard DIMACS CNF format.
./SATzillaX <path_to_cnf_file>(On Windows, run SATzillaX.exe <path_to_cnf_file>)
The output follows standard SAT competition formatting:
- If the formula is satisfiable:
(Positive integers represent
SAT <assigned_literals> 0truevariables, negative integers representfalsevariables, terminated by a0) - If the formula is unsatisfiable:
UNSAT
Consider a simple CNF formula representing
example_sat.cnf:
c Example satisfiable formula
p cnf 3 3
1 2 0
-1 3 0
-2 -3 0
Running the Solver:
./SATzillaX example_sat.cnfExpected Output:
SAT
1 -2 3 0
(Meaning: $x_1 = \text{true}$, $x_2 = \text{false}$, $x_3 = \text{true}$ satisfies the formula)
Consider a simple contradiction:
example_unsat.cnf:
c Example unsatisfiable formula
p cnf 1 2
1 0
-1 0
Running the Solver:
./SATzillaX example_unsat.cnfExpected Output:
UNSAT
- Pre-processing / Parsing: The input DIMACS CNF file is tokenized into raw integers. Single-literal unit clauses are propagated immediately.
- Decide (Branching): Variables are picked based on their VSIDS scores (variables involved in conflicts get higher weights).
- Propagate (BCP): The 2-watched-literals scheme propagates assignments. If a conflict occurs:
- Analyze Conflict: The solver backtracks along the implication graph to find the 1st UIP, constructs a learned clause, and adds it to the database.
- Backjump: The solver performs non-chronological backtracking to the decision level where the learned clause becomes unit, enabling immediate propagation of the implication.
- Restart: Periodically, the solver clears assignments and restarts the search from decision level 0, using the learned clauses and saved phases to explore a different region of the search space.
This project is licensed under the MIT License. See below or refer to the repository LICENSE file for details.
MIT License
Copyright (c) 2026 Satvik Jambagi
Permission is hereby granted, free of charge, to any person obtaining a copy
of this software and associated documentation files (the "Software"), to deal
in the Software without restriction, including without limitation the rights
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all
copies or substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
SOFTWARE.
- Developer: Satvik Jambagi
- GitHub: @7vik2005