The satisfiability problem (SAT) is a typical NP-complete problem where a wide range of applications has been studied. Given a set of variables U and a set of clauses C, the goal of SAT is to find a truth assignment to variables in U such that every clause in C is satisfied if it exits, or to derive the infeasibility otherwise. This paper presents an approximation algorithm called a minimal-state processing search algorithm for SAT (MIPS_SAT). MIPS_SAT repeatedly transits minimal states in terms of the cost function for searching a solution through a construction stage and a refinement stage. The first stage greedily generates an initial state composed of as many satisfied clauses as possible. The second stage iteratively seeks a solution while keeping state minimality. The performance of MIPS_SAT is verified through solving DIMACS benchmark instances.
|Number of pages||6|
|Journal||Proceedings of the IEEE International Conference on Systems, Man and Cybernetics|
|Publication status||Published - Jan 1 2001|
- Heuristic algorithm
ASJC Scopus subject areas
- Control and Systems Engineering
- Hardware and Architecture