Document Type

Technical Report

Department

Computer Science and Engineering

Publication Date

2006-01-01

Filename

wucse-2006-1.pdf

Technical Report Number

WUCSE-2006-1

Abstract

Limit crossing is a methodology in which modified versions of a problem are solved and compared, yielding useful information about the original problem. Pruning rules that are used to exclude portions of search trees are excellent examples of the limit-crossing technique. In our previous work, we examined limit crossing for optimization problems. In this paper, we extend this methodology to decision problems. We demonstrate the use of limit crossing in our design of a tool for identifying K-SAT backbones. This tool is guaranteed to identify all of the backbone variables by solving at most n+1 formulae, where n is the total number of variables. While previous 3-SAT backbone research was limited to 28 variables, we have computed backbones for 200 variables. In addition to being useful for identifying backbones, this code can be used directly to solve a special class of QBF problems

Comments

Permanent URL: http://dx.doi.org/10.7936/K77S7KZK

Download

Share

COinS