Wyniki wyszukiwania - BazTech

Ograniczanie wyników

Znaleziono wyników: 1

Liczba wyników na stronie

Wyniki wyszukiwania

Wyszukiwano:
w słowach kluczowych: logiczne formuły w postaci CNF

Sortuj według:

Ogranicz wyniki do:

An effective SAT-Solving mechanism with backtrack controlled by FDL

Pułka A.

Elektronika : konstrukcje, technologie, zastosowania

2011

Vol. 52, nr 12

21-25

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.

Artykuł przedstawia nowe podejście do problemu badania spełnialności formuł logicznych oparte na metodzie wnioskowania zdroworozsądkowego. Zaproponowana metoda została zaimplementowana i przetestowana w środowisku języka PROLOG. Przeprowadzono szczegółową dyskusję dotyczącą istniejących nowoczesnych technik sprawdzania spełnialności formuł logicznych, które zostały opublikowane w ostatnich latach. Przedstawiono podobieństwa między problemem badania spełnialności formuł logicznych a weryfikacją rozszerzeń w logice niemonotonicznej. Sformułowano podstawowe założenia nowego algorytmu FUDASAT badania spełnialności formuł logicznych opartego na wnioskowaniu FDL oraz zdefiniowano problem kumulacyjności formuł w postaci normalnej CNF. Metoda optymalnego przeszukiwania podczas nawrotów została opisana na przykładach. Eksperymenty przeprowadzone na zestawach wzorcowych pokazują zalety proponowanej metody.