@inproceedings{43f6e49a3b224c7981de417a6d285191,
title = "An effective SAT-solving mechanism with backtrack controlled by FDL",
abstract = "This work presents a novel approach to SAT solving problem based on commonsense reasoning methodology. The methodology has been implemented and tested in PROLOG. Discussion of different modern approaches to the satisfiability that have been published recently is presented. A parallelism between the SAT solving problem and non-monotonic extensions verifying is given. The new algorithm of SAT solving based on fuzzy default reasoning (FDL) theory FUDASAT and cumulativity of CNF formulas is defined. Optimal backtracking search methodology is explained on examples. Some experiments on various benchmarks show the efficiency and advantages of the proposed methodology.",
keywords = "Boolean satisfiability, CNF, Formal verification, SAT solving",
author = "Andrzej Pu{\l}ka",
year = "2011",
language = "English",
isbn = "9788393207503",
series = "Proceedings of the 18th International Conference - Mixed Design of Integrated Circuits and Systems, MIXDES 2011",
pages = "252--257",
booktitle = "Proceedings of the 18th International Conference - Mixed Design of Integrated Circuits and Systems, MIXDES 2011",
note = "18th International Conference - Mixed Design of Integrated Circuits and Systems, MIXDES 2011 ; Conference date: 16-06-2011 Through 18-06-2011",
}