<abstract xmlns="http://www.w3.org/1999/xhtml"><p>The paper concerns the problem of Boolean satisﬁability checking, which is recognized as one of the most important issues in the ﬁeld of modern digital electronic system veriﬁcation and design. The paper analyzes different strategies and scenarios of the proving process, and presents a modiﬁed and extended version of the author’s FUDASAT algorithm. The original FUDASAT methodology is an intuitive approach that employs a commonsense reasoning methodology. The main objective of the work is to investigate the SAT-solving process and try to formulate a set of rules controlling the reasoning process of the FUDASAT inference engine. In comparison with the author’s previous works, the paper introduces new mechanisms: hypergraph analysis, multiple variable assignments and search space pruning algorithms. The approach considers only 3-SAT class functions, although a generalization of the method is discussed as well. The presented approach has been tested on various benchmarks and compared with the original pure FUDASAT algorithm as well as with other algorithms known from the literature. Finally, the beneﬁts of the proposed SAT solving technique are summarized.</p></abstract>

The paper concerns the problem of Boolean satisﬁability checking, which is recognized as one of the most important issues in the ﬁeld of modern digital electronic system veriﬁcation and design. The paper analyzes different strategies and scenarios of the proving process, and presents a modiﬁed and extended version of the author’s FUDASAT algorithm. The original FUDASAT methodology is an intuitive approach that employs a commonsense reasoning methodology. The main objective of the work is to investigate the SAT-solving process and try to formulate a set of rules controlling the reasoning process of the FUDASAT inference engine. In comparison with the author’s previous works, the paper introduces new mechanisms: hypergraph analysis, multiple variable assignments and search space pruning algorithms. The approach considers only 3-SAT class functions, although a generalization of the method is discussed as well. The presented approach has been tested on various benchmarks and compared with the original pure FUDASAT algorithm as well as with other algorithms known from the literature. Finally, the beneﬁts of the proposed SAT solving technique are summarized.

Selection of search strategies for solving 3-SAT problems

Institute of Electronics Silesian University of Technology, ul. Akademicka 16, 44-100 Gliwice, Poland

International Journal of Applied Mathematics and Computer Science

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Selection of search strategies for solving 3-SAT problems"}

The paper concerns the problem of Boolean satisﬁability checking, which is recognized as one of the most important issues in the ﬁeld of modern digital...

Selection of search strategies for solving 3-SAT problems

Publié en ligne: 26 juin 2014

Pages: 283 - 297

Reçu: 13 janv. 2013

DOI: https://doi.org/10.2478/amcs-2014-0021

Mots clés
SAT solving, formal veriﬁcation, CNF, Boolean satisﬁability

© 2014 Andrzej Pułka

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Selection of search strategies for solving 3-SAT problems

Publié en ligne: 26 juin 2014

Pages: 283 - 297

Reçu: 13 janv. 2013

DOI: https://doi.org/10.2478/amcs-2014-0021

Mots clésSAT solving, formal veriﬁcation, CNF, Boolean satisﬁability

© 2014 Andrzej Pułka

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Mots clés
SAT solving, formal veriﬁcation, CNF, Boolean satisﬁability