## FORMULA DISSECTION: A PARALLEL ALGORITHM FOR CONSTRAINT SATISFACTION.

Publication
, Journal Article

Kasif, S; Reif, JH; Sherlekar, DD

December 1, 1987

The authors present a simple and relatively efficient divide-and-conquer method to solve various subclasses of SAT (the problem of testing satisfiability of propositional formulas). The dissection stage of the algorithm splits the original formula into smaller subformulae with only a bounded number of interacting variables. In particular, the authors derive an algorithm with a worst-case performance of 2**c** ROOT **n for planar 3-SAT, the class of formulas whose corresponding graph representation is planar. An application of the method to constraint-satisfaction problems is discussed. A parallel implementation of the algorithm on a shared-memory parallel computer is presented.

### Duke Scholars

## Publication Date

December 1, 1987

## Start / End Page

51 / 58

### Citation

APA

Chicago

ICMJE

MLA

NLM

Kasif, S., Reif, J. H., & Sherlekar, D. D. (1987). FORMULA DISSECTION: A PARALLEL ALGORITHM FOR CONSTRAINT SATISFACTION., 51–58.

Kasif, S., J. H. Reif, and D. D. Sherlekar. “FORMULA DISSECTION: A PARALLEL ALGORITHM FOR CONSTRAINT SATISFACTION.,” December 1, 1987, 51–58.

Kasif S, Reif JH, Sherlekar DD. FORMULA DISSECTION: A PARALLEL ALGORITHM FOR CONSTRAINT SATISFACTION. 1987 Dec 1;51–8.

Kasif, S., et al.

*FORMULA DISSECTION: A PARALLEL ALGORITHM FOR CONSTRAINT SATISFACTION.*Dec. 1987, pp. 51–58.Kasif S, Reif JH, Sherlekar DD. FORMULA DISSECTION: A PARALLEL ALGORITHM FOR CONSTRAINT SATISFACTION. 1987 Dec 1;51–58.

## Publication Date

December 1, 1987

## Start / End Page

51 / 58