SAT 2004 START ConferenceManager    


A Note on Satisfying Truth-Value Assignments of Boolean Formulas

Zbigniew Stachniak

Presented at The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada, 10-13 May 2004


Abstract

In this paper a class of truth-value assignments, called bounded assignments, is defined using a certain substitutional property. It is shown that every satisfiable Boolean formula has at least one bounded assignment. If a Boolean formula has just one satisfying truth-value assignment, then such an assignment is bounded and, in addition, it can be syntactically defined (characterized) in the language of classical propositional logic.

The theoretical properties of bounded truth-value assignments can be used to derive search heuristics for complete and incomplete algorithms for solving Boolean satisfiability problems. As an example, we show that WalkSAT's local search heuristic derives naturally from the characterization of a bounded truth-value assignment.


  
START Conference Manager (V2.47.2)
Maintainer: rrgerber@softconf.com