Investigation of Efficient Heuristics for a
State-Based Satisfiability Solver

Shikha Goyal, Anne Cross, John Franco
Department of Computer Science
University of Cincinnati, Ohio, USA

Supported by a grant from the
Computer Research Association
Committee on the Status of Women in Computing Research
and the
National Science Foundation

 

Project Description
    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 [3] 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.

References
    [1] "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 Science 12(10):1655-1692, 2004.

[2] "State-based propositional Satisfiability Solver," J. Franco, M. Dransfield, W.M. Vanfleet, J.S. Schlipf. US Patent number 6,912,700, 2005.

[3] "A machine program for theorem proving," M. Davis, G. Logemann, and D. Loveland. Communications of the ACM 5:394-397, 1962.

Available Resources
    Faculty and students have computers on which to perform the implementation and experiments. SBSAT exists, can be modified, and can be extended.

Expected Effort
   
1.    About 30% of the project involves creative effort: that is, inventing ideas for efficient search from pattern analysis.
2.    About 50% of the project involves implementing and modifying software and documenting results;
3.    About 20% of the project involves running experiments and analyzing results;

Time-line
   

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
   
1.    Study the Satisfiability problem. Understand why it is hard, in general
2.    Get to know some important applications of this problem
3.    Study proposed solutions and systems. That is, research and understand what is known about structural properties of CNF formulas and how existing systems exploit those properties to speed up computation. In particular, investigate the use of symmetry breaking in Satisfiability solving
4.    Understand the effect of inference finding and learning on the speed of a Satisfiability solver
5.    Learn how to use and understand the capabilities of SBSAT
6.    Propose and implement effective heuristics for certain benchmarks, to be determined later, based on knowledge gained from the above
7.    Record results of experiments
8.    Repeat the above two points with refinements
9.    Document all results
10.    Publish at least one paper in a Satisfiability journal or conference

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.