Browse Prior Art Database

Method and System for Satisfiability Solving taking advantage of Information derived from Circuit Structure and Binary-Decision-Diagram Sweeping

IP.com Disclosure Number: IPCOM000031632D
Original Publication Date: 2004-Oct-01
Included in the Prior Art Database: 2004-Oct-01

Publishing Venue

IBM

Abstract

Proposed is a new method for selecting the next decision variable in a structural SAT solver. The next decision variable is selected from among those on the justification frontier using a score that includes circuit topology information together with partitioning information (cut-frontiers) obtained by propagating BDDs through the circuit using BDD-sweeping. This method prioritizes the vertices in the justification frontier based on the cut-levels identified by BDD-sweeping, which effectively localizes the search space for the SAT solver, helping it to solve the problem more quickly by potentially pruning large portions of the search space.