SAT solvers address the satisfiability problem of Boolean formulas, forming the basis of many computational and verification tasks.
Our Research Focus
Local Search Based Algorithms
Focus on heuristic-driven search strategies to efficiently solve large, satisfiable instances. Our research explores:
- Advanced variable selection heuristics
- Novel scoring functions
- Efficient neighborhood exploration techniques
- Dynamic strategy adaptation
Hybrid Algorithms
Combine complete solvers (e.g. CDCL) with local search methods to leverage the strengths of both approaches:
- Integration of CDCL and local search
- Dynamic switching mechanisms
- Learned clause sharing strategies
- Hybrid preprocessing techniques
Distributed Solvers
Explore parallel and distributed computing to tackle large-scale SAT problems through:
- Search space division strategies
- Load balancing techniques
- Efficient clause sharing protocols
- Scalable architecture design
- Job scheduling optimization
Our group has developed several state-of-the-art SAT solvers:
- PRS: A parallel SAT solver framework
- Relaxed: A hybrid algorithm SAT solver
- CCAnr: A local search SAT solver with preprocessing