State-Based Satisfiability Solver
Shikha Goyal, Anne Cross, John Franco
Supported by a grant from the
|The proposed project aims to enhance a next-generation Satisfiability
solver, called SBSAT [1,2], for use on problems arising in areas of
Information Assurance. SBSAT offers significantly improved
performance in finding solutions to a number of frequently encountered
and important logic-based problems, many of which have their origins
in Information Assurance. Specifically, the solver is intended to
assist software and hardware designers in completing tasks which
increase component, system, and network reliability. Such tasks
include verification that safety, security, and integrity requirements
are met or exceeded; and detection of errors that may lead to a system
failure condition. By safety and security we mean a system must do
exactly what it is intended to do and do nothing more. Typically, if
a system is allowed to do more than what it is intended to do there is
a risk of an intruder exploiting forbidden states to mangle, or view
sensitive and confidential data.
Satisfiability solvers have been developed for the purpose of finding solutions to large Boolean formulas. About 15 years ago the state-of-the-art was such that these solvers were too slow to have any practical application. But enormous progress has been made over the years so that now many problems which had been thought to be extremely difficult in 1990 are now considered trivial. However, many difficult problems remain. We, and other groups, are currently investigating ways to deal with them. In particular, difficult problems of critical importance, for example those relating to Information Assurance, are the target for many groups, including ours.
SBSAT is currently implemented in software. It features a powerful preprocessor that is able to collect, analyze, and memorize domain-specific information in highly sophisticated ways so that it may be used effectively and efficiently during search for solutions. Up to now the full potential for improving search in SBSAT has not been exploited. It is the goal of this project to determine new ways to do that. Specifically, this project aims to develop advanced search heuristics for the improved solution of a number of well-known and difficult benchmarks. Investigation of heuristics will undoubtedly suggest improvements in preprocessor design.
Most conventional solvers are based on the Davis-Putnam-Loveland-Logemann (DPLL) algorithm  for solving Conjunctive Normal Form Boolean (CNF) formulas. At the heart of this algorithm is a search process in which some variables are given values and tests are made to see whether it is impossible to extend this assignment of values to a larger one without violating the formula. If not, further extensions are made until either it is impossible to continue with the current assignment or a solution is found. In the latter case, the solution is reported and the algorithm terminated, but in the former case values are removed from some assigned variables and the extension process repeated with different assignments. Due to all the possibilities for assigning and unassigning variables, the search may take a long time. The set of all the intermediate assignments visited during the execution of the algorithm is called the search space. Choosing assignments during search is the job of the search heuristic. A good search heuristic may result in a search space that is orders of magnitude smaller than one explored by a bad search heuristic. Hence the design of search heuristics is extremely important. What constitutes a good search heuristic is highly dependent on the particular type of formula that is being solved.
Finding search heuristics for SBSAT differs from finding search heuristics for conventional Satisfiability solvers in one crucial respect: conventional solvers must translate Boolean formulas into CNF formulas before solving them. Doing so typically garbles parts of the original formulas which express domain-specific information. Domain-specific information is often crucial for search heuristics to prune significant portions of the search space. SBSAT does no such translation. Therefore, SBSAT has the potential for the development of advanced search heuristics that are far beyond what is possible with conventional solvers. We intend to exploit this advantage as much as we can.
| "Function-complete look-ahead in support of efficient SAT search
heuristics," J. Franco, M. Kouril, J.S. Schlipf, S. Weaver,
M. Dransfield, W.M. Vanfleet. Journal of Universal Computer
 "State-based propositional Satisfiability Solver," J. Franco, M. Dransfield, W.M. Vanfleet, J.S. Schlipf. US Patent number 6,912,700, 2005.
 "A machine program for theorem proving," M. Davis, G. Logemann, and D. Loveland. Communications of the ACM 5:394-397, 1962.
|Faculty and students have computers on which to perform the implementation and experiments. SBSAT exists, can be modified, and can be extended.|
Impact on the Goals of CREU
|This research supports state-of-the-art advances in a field which is increasingly important to applications in Computer Science, Computer Engineering, and Operations Research, among other. A few years ago, Satisfiability was not even thought of as a research area. Now there are major conferences and journals that are focused on this area. Therefore, contributions that we make as a result of this research will be the stepping stones to significant, timely, highly visible, advanced research, specifically in Satisfiability, but more generally in theoretical computer science. Such topics are quite suitable for Masters and even Ph.D. theses. Thus, this research project will have a direct bearing on the professional future of its participants and their influence on the technical community. In achieving success, both on this project, and on future research projects, we expect our professional path to become a model by which other women can achieve similar success.|
Student Activity and Responsibility
Faculty Activity and Responsibility
|Prof. Franco will supervise the project and supply needed software. Weekly meetings will be held in Prof. Franco's office to discuss progress and direction. A record of each meeting will be kept with Prof. Franco. Prof. Franco will not engage directly in the research but may make suggestions on what direction to take. All research results will come directly from the students.|