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, 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.  (more)   (references)

Questions Addressed
   
1.    What search heuristics are optimal for certain specified benchmarks, for example benchmarks intending to "prove" the equivalence of two circuits?
2.    What domain-specific information do the proposed heuristics require?
3.    How can the preprocessor be directed to efficiently collect that data for the proposed heuristics?

Methods
    This project requires the following steps:
1.    Analysis of benchmark instances for exploitable, functional patterns;
2.    Proposal of a heuristic to exploit those patterns;
3.    Analysis of the need to support that heuristic in the preprocessor;
4.    Implementation of the changes to the preprocessor and the proposed heuristic;
5.    Experiments on the benchmarks to validate ideas.

Miscellany
    Available resources
    Expected effort
    Time-line
    Impact on the goals of CREU
    Student activity and responsibility
    Faculty activity and responsibility

Biographical Sketches
    Anne Cross
    Shikha Goyal
    John Franco

Meeting Notes
    28 Aug 2006     First meeting - install Linux on Goyal's laptop, discuss Satisfiability, Search.
    20 Sep 2006     Second meeting - discuss Satisfiability, DPLL, BDD, ind & dep variables, heuristics.
    27 Sep 2006     BDDs, preprocessing, sbsat switches.
    04 Oct 2006     Solving Sudoku using a SAT solver
    11 Oct 2006     Short meeting - taking stock.
    18 Oct 2006     Controlling variable elimination, Sliders, Cores.
    25 Oct 2006     Controlling variable elimination, Sliders, Cores.
    1 Nov 2006     Controlling variable elimination, Sliders, Cores.
    8 Nov 2006     Sliders and Cores.
    15 Nov 2006     Reassessment and assignment
    22 Nov 2006     Sliders and Cores.
    11 Jan 2007     Hard cores for sliders - results of experiments.
    18 Jan 2007     Discussion of experimental results - proposals for next week.
    25 Jan 2007     Discussion of experimental results - proposals for next week.
    1 Feb 2007     Multi-function conflicts and their possible relationship to the hard core.
    8 Feb 2007     Multi-function conflicts and their possible relationship to the hard core.
    15 Feb 2007     Possible revelation - anticipating lemmas!
    22 Feb 2007     Continuing on the revelation
    01 Mar 2007     Still continuing on the revelation
    28 Mar 2007     -
    4 Apr 2007     -
    11 Apr 2007     -
    18 Apr 2007     -
    25 Apr 2007     -
    2 May 2007     Adding search heuristics to SBSAT
    9 May 2007     Adding search heuristics to SBSAT

Noteworthy Results and Reports
    Cross notes, early January, 2007     Notes from experiments on finding "hard core" for 60 variable slider.
    Cross notes, middle January, 2007     Observations on moving toward "heavy tail" analysis.
    Cross notes, end January, 2007     Record of "heavy tail" experiments.
    Goyal notes, end January, 2007     Record of "heavy tail" experiments.