Буле қанағаттандыру мәселелерін шешуге арналған GSAT және WalkSAT алгоритмдері
WalkSAT
Буле қанағаттандыру мәселесін шешетін GSAT және WalkSAT алгоритмдері туралы мақала. Локалды іздеу әдістері, Boolean логикасы, және айнымалыларды өзгерту қарастырылады.
Ағылшыншамен салыстырыңыз: абзацты басыңыз — түпнұсқа терезеде ашылады. Абзац астындағы EN түймесі оны мәтін ішінде көрсетеді.
Кіріспе
Компьютерлік ғылымда GSAT және WalkSAT – Бульдық қанағаттандыру мәселелерін шешуге арналған жергілікті іздеу алгоритмдері. Екі алгоритм де Буль логикасындағы формулалармен жұмыс істейді, олар конъюнктивті қалыпты түрге келтірілген немесе оған түрлендірілген. Олар формуланың әрбір айнымалысына кездейсоқ мән тағайындаудан бастайды. Егер тағайындама барлық шарттарды қанағаттандырса, алгоритм аяқталады және тағайындаманы қайтарады. Әйтпесе, бір айнымалының мәні өзгертіліп, барлық шарттар орындалғанға дейін жоғарыдағы әрекет қайталанады. WalkSAT және GSAT айнымалыны өзгертуді таңдау әдістерімен ерекшеленеді. GSAT жаңа тағайындамада қанағаттандырылмаған шарттардың санын азайтатын өзгерісті жасайды немесе белгілі бір ықтималдықпен кездейсоқ айнымалыны таңдайды. WalkSAT ең алдымен ағымдағы тағайындамамен қанағаттандырылмаған шартты таңдайды, содан кейін осы шарттағы айнымалыны өзгертеді. Шарт қанағаттандырылмаған шарттардың арасынан кездейсоқ таңдалады. Бұрын қанағаттандырылған шарттардың ең азын қанағаттандырылмауына әкелетін айнымалы таңдалады, бірақ айнымалылардың біреуін кездейсоқ таңдау мүмкіндігі де қарастырылады. Кездейсоқ таңдағанда, WalkSAT шарттағы айнымалылардың санына тең немесе одан да көп мүмкіндікке ие, қазіргі уақытта дұрыс емес тағайындаманы түзетуге. Оптималды айнымалыны таңдағанда WalkSAT GSAT-қа қарағанда аз есептеулер жасайды, өйткені ол азырақ мүмкіндіктерді қарастырады. Егер шешім ұзақ уақыттан бері табылмайтын болса, екі алгоритм де қанағаттандырылмаған шарттар санының жергілікті минимумдарынан шығу үшін жаңа кездейсоқ тағайындамамен қайта басталуы мүмкін. GSAT және WalkSAT-тың көптеген нұсқалары бар. WalkSAT автоматтандырылған жоспарлау мәселелерінен аударма арқылы туындаған қанағаттандыру мәселелерін шешуде ерекше пайдалы болып көрінді. Жоспарлау мәселелерін Бульдық қанағаттандыру мәселелеріне түрлендіретін жоспарлау тәсілі satplan деп аталады. MaxWalkSAT – WalkSAT-тың нұсқасы, ол салмақталған қанағаттандыру мәселесін шешуге арналған, онда әр шартқа салмақ сәйкес келеді және мақсат – бүкіл формуланы қанағаттандыратын немесе қанағаттандырмайтын тағайындаманы табу, осы тағайындамамен қанағаттандырылған шарттардың жалпы салмағын барынша арттыру.
In computer science, GSAT and WalkSAT are local search algorithms to solve Boolean satisfiability problems. Both algorithms work on formulae in Boolean logic that are in, or have been converted into conjunctive normal form. They start by assigning a random value to each variable in the formula. If the assignment satisfies all clauses, the algorithm terminates, returning the assignment. Otherwise, a variable is flipped and the above is then repeated until all the clauses are satisfied. WalkSAT and GSAT differ in the methods used to select which variable to flip. GSAT makes the change which minimizes the number of unsatisfied clauses in the new assignment, or with some probability picks a variable at random. WalkSAT first picks a clause which is unsatisfied by the current assignment, then flips a variable within that clause. The clause is picked at random among unsatisfied clauses. The variable is picked that will result in the fewest previously satisfied clauses becoming unsatisfied, with some probability of picking one of the variables at random. When picking at random, WalkSAT is guaranteed at least a chance of one out of the number of variables in the clause of fixing a currently incorrect assignment. When picking a guessed to be optimal variable, WalkSAT has to do less calculation than GSAT because it is considering fewer possibilities. Both algorithms may restart with a new random assignment if no solution has been found for too long, as a way of getting out of local minima of numbers of unsatisfied clauses. Many versions of GSAT and WalkSAT exist. WalkSAT has been proven particularly useful in solving satisfiability problems produced by conversion from automated planning problems. The approach to planning that converts planning problems into Boolean satisfiability problems is called satplan. MaxWalkSAT is a variant of WalkSAT designed to solve the weighted satisfiability problem, in which each clause has associated with a weight, and the goal is to find an assignment—one which may or may not satisfy the entire formula—that maximizes the total weight of the clauses satisfied by that assignment.