Czasopismo | ELEKTRONIKA - KONSTRUKCJE, TECHNOLOGIE, ZASTOSOWANIA | Rocznik 2011 - zeszyt 12

An effective SAT-Solving mechanism with backtrack controlled by FDL

Andrzej Pułka

nr katalogowy: 64767

The problem of Boolean satisfiability (SAT) has been recognized since the beginning of logical circuits existence and belongs to one of the most studied issues in the field of combinatorial search and minimization as well as Artificial Intelligence problems. Many works devoted to SAT solvers [1, 2, 5-8, 10, 11], i.e. methods and algorithms for solving the Boolean satisfiablity tasks bore fruits in practical applications as packages embedded into Electronic Design Automation (EDA) tools. Sat solvers are commonly used for testing in automated test patterns generators [13]. The presented paper introduces some modifications to existing approaches in a for of a new original SAT-solving algorithm supported with optimal selection of variables and backtrack search controlling mechanisms based on the technique borrowed from AI - fuzzy default logic (FDL). Problem description and related works The problem of Boolean satisfiability (SAT) can be formulated as follows: verify and prove that there exists (or does not exist) an assignment (of variables) for a given Boolean function F for which the function is satisfied (evaluates to true). Usually a SAT task belongs to NP-complete problems and its solving is not trivial. The problem specification Usually the SAT problems are presented in standard conjunctive normal form (CNF), i.e. as a conjunction of clauses Ci, where every clause is given as a disjunction of literals. Each literal comprises the elementary logical unit of a given Boolean function F (problem), being merely an instance of a variable or its complement. Formally, for a given Boolean function F(x1,…, xN) of variables X = {x1, ¬x1,…, xN, ¬xN} (where symbol ¬xi denotes the complemented variable), we can express the function F in CNF form as: (1) The main advantage of such a formulation (CNF) of the problem is the practical meaning (reduction) of SAT. In order to prove the satisfiability of a given CNF[...]

Jeśli masz wykupiony/przyznany dostęp - zaloguj się. Skorzystaj z naszych propozycji zakupu!

Publikacja


e-Publikacja (format pdf) - nr 64767 "An effective SAT-Solving ..." licencja: Osobista Produkt cyfrowy	10.00 zł

Zeszyt


ELEKTRONIKA - KONSTRUKCJE, TECHNOLOGIE, ZASTOSOWANIA - e-zeszyt (pdf) 2011-12 licencja: Osobista Produkt cyfrowy	35.00 zł

Prenumerata

ELEKTRONIKA - KONSTRUKCJE, TECHNOLOGIE, ZASTOSOWANIA - prenumerata cyfrowa
licencja: Osobista

Produkt cyfrowy
Nowość

420.00 zł

ELEKTRONIKA - KONSTRUKCJE, TECHNOLOGIE, ZASTOSOWANIA - papierowa prenumerata roczna + wysyłka
licencja: Osobista

Szczegóły pakietu

Nazwa
ELEKTRONIKA - KONSTRUKCJE, TECHNOLOGIE, ZASTOSOWANIA - papierowa prenumerata roczna	528.00 zł brutto 488.89 zł netto 39.11 zł VAT (stawka VAT 8%)
ELEKTRONIKA - KONSTRUKCJE, TECHNOLOGIE, ZASTOSOWANIA - pakowanie i wysyłka	42.00 zł brutto 34.15 zł netto 7.85 zł VAT (stawka VAT 23%)

570.00 zł

ELEKTRONIKA - KONSTRUKCJE, TECHNOLOGIE, ZASTOSOWANIA - PAKIET prenumerata PLUS
licencja: Osobista

Szczegóły pakietu

Nazwa
ELEKTRONIKA - KONSTRUKCJE, TECHNOLOGIE, ZASTOSOWANIA - PAKIET prenumerata PLUS (Prenumerata papierowa + dostęp do portalu sigma-not.pl + e-prenumerata)	636.00 zł brutto 588.89 zł netto 47.11 zł VAT (stawka VAT 8%)

636.00 zł

Zeszyt

2011-12

Twój Koszyk

Publikacja

Zeszyt

Prenumerata

Zeszyt

Czasopisma