Speculative Pruning for Boolean Satisfiability

DSpace/Manakin Repository

Speculative Pruning for Boolean Satisfiability

Citable link to this page


Title: Speculative Pruning for Boolean Satisfiability
Author: Ruml, Wheeler; Ginsburg, Adam; Shieber, Stuart Merrill ORCID  0000-0002-7733-8195

Note: Order does not necessarily reflect citation order of authors.

Citation: Ruml, Wheeler, Adam Ginsburg, and Stuart Shieber. Speculative Pruning for Boolean Satisfiability. Harvard Computer Science Group Technical Report TR-02-99.
Full Text & Related Files:
Abstract: Much recent work on boolean satisfiability has focussed on incomplete algorithms that sacrifice accuracy for improved running time. Statistical predictors of satisfiability do not return actual satisfying assignments, but at least two have been developed that run in linear time. Search algorithms allow increased accuracy with additional running time, and can return satisfying assignments. The efficient search algorithms have been proposed are based on iteratively improving a random assignment, in effect searching a graph of degree equal to the number of variables. In this paper, we examine an incomplete algorithm based on searching a standard binary tree, in which statistical predictors are used to speculatively prune the tree in constant time. Experimental evaluation on hard random instances shows it to be the first practical incomplete algorithm based on tree search, surpassing even graph-based methods on smaller instances.
Terms of Use: This article is made available under the terms and conditions applicable to Other Posted Material, as set forth at http://nrs.harvard.edu/urn-3:HUL.InstRepos:dash.current.terms-of-use#LAA
Citable link to this page: http://nrs.harvard.edu/urn-3:HUL.InstRepos:23518799
Downloads of this work:

Show full Dublin Core record

This item appears in the following Collection(s)


Search DASH

Advanced Search