New Boolean satisfiability problem heuristic strategy: Minimal Positive Negative Product Strategy
This work addresses the Boolean satisfiability problem for researchers and practitioners in computational logic and AI, offering an incremental improvement in heuristic design.
The authors tackled the Boolean satisfiability problem by introducing the Minimal Positive Negative Product Strategy, a novel heuristic for the CDCL algorithm, which they mathematically explained and experimentally validated as more effective than existing heuristics like DLIS and VSIDS.
This study presents a novel heuristic algorithm called the "Minimal Positive Negative Product Strategy" to guide the CDCL algorithm in solving the Boolean satisfiability problem. It provides a mathematical explanation for the superiority of this algorithm over widely used heuristics such as the Dynamic Largest Individual Sum (DLIS) and the Variable State Independent Decaying Sum (VSIDS). Experimental results further confirm the effectiveness of this heuristic strategy in problem-solving.