MiniSat v1.13 - A SAT Solver with Conflict-Clause Minimization
Generate an AI Snapshot to get a quick, structured summary of this paper.
A concise AI-generated summary of the paper will appear here once you click Generate AI Snapshot.
TL;DR
The particular version of VSIDS in MiniSat is believed to be a consistent improvement over the original VSIDS decision heuristic of the same magnitude as many of the recently proposed alternatives (GY02,Ry03).
Abstract
In this poster we summarize the features of the MiniSat version en- tering the SAT Competition 2005. The main new feature is a resolution based conflict clause minimization technique based on self-subsuming resolution. Ex- periments show that on industrial examples, it is not unusual for more than 30% of the literals in a conflict clause to be redundant. Removing these literals re- duces memory consumption and produce stronger clauses which may propagate under fewer decisions in the DPLL search procedure. We also want to raise attention to the particular version of VSIDS im- plemented in MiniSat, which we believe is a consistent improvement over the original VSIDS decision heuristic of the same magnitude as many of the recently proposed alternatives (GY02,Ry03).