本研究の目的は，和積形論理式の充足可能性問題（SAT）の解法アルゴリズムである局所探索法の高速化である．局所探索法のアルゴリズムGSATに対し，実働化時の工夫と並列化によって高速化を試みる．SelmanとKautzのGSATを元に，(i)~データ構造の改良，(ii)~ベクトル並列計算機上でのベクトル化，(iii)~PVMを使った40? CPUによる並列化，を行った．これにより，合計600倍の高速化を達成した．2nd DIMACS Implementation Challenge Satisfiabilityのベンチマーク例題に対して我々のGSATを実行させたところ，既存のプログラムで解けている例題では実行時間がかなり短縮された．また，GSATを改良した局所探索法に本論文の手法を適用させることにより，既存のプログラムでは解けなかった例題を解くまでに至った．The purpose of this paper is to speed up the local search algorithmfor CNF Satisfiability problem by implementation techniques andparallelization. We selected GSAT by Selman and Kautz and attemptedspeedup by the following techniques: (i)~An improvement of the datastructure of Selman and Kautz's implementation. (ii)~Vectorization ona parallel vector supercomputer. (iii)~Parallelization using ParallelVirtual Machine (PVM). By these attempts, we achieved 600-timesspeedup in total. We executed our GSAT for benchmark instances of the2nd DIMACS Implementation Challenge, Satisfiability. Our programperformed much better than existing programs on most instances.Moreover, we were able to solve some instances that existing programscould not have solved.