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.