Using Grover's search quantum algorithm to solve Boolean satisfiability problems, part 2

2019 ◽  
Vol 26 (2) ◽  
pp. 68-71
Author(s):  
Diogo Fernandes ◽  
Carla Silva ◽  
Inês Dutra
Keyword(s):  
Quantum Algorithm ◽  
Boolean Satisfiability ◽  
Satisfiability Problems

scholarly journals The approximability of non-Boolean satisfiability problems and restricted integer programming

2005 ◽  
Vol 332 (1-3) ◽  
pp. 123-139 ◽  
Author(s):  
Maria Serna ◽  
Luca Trevisan ◽  
Fatos Xhafa
Keyword(s):  
Integer Programming ◽  
Boolean Satisfiability ◽  
Satisfiability Problems

Solving Non-Boolean Satisfiability Problems with Stochastic Local Search: A Comparison of Encodings

2006 ◽  
Vol 35 (1-3) ◽  
pp. 143-179 ◽  
Author(s):  
Alan M. Frisch ◽  
Timothy J. Peugniez ◽  
Anthony J. Doggett ◽  
Peter W. Nightingale
Keyword(s):  
Local Search ◽  
Boolean Satisfiability ◽  
Stochastic Local Search ◽  
Satisfiability Problems

scholarly journals Duplicates of conflict clauses in CDCL derivation and their usage to invert some cryptographic functions

2019 ◽  
pp. 54-66
Author(s):  
В.С. Кондратьев ◽  
А.А. Семенов ◽  
О.С. Заикин
Keyword(s):  
Hash Functions ◽  
Boolean Satisfiability ◽  
Experimental Results ◽  
Sat Solving ◽  
New Approach ◽  
Sat Solvers ◽  
Satisfiability Problems ◽  
Clause Learning ◽  
Sat Solver ◽  
Cryptographic Hash Functions

Изучен феномен повторного порождения конфликтных ограничений SAT-решателями в процессе работы с трудными экземплярами задачи о булевой выполнимости. Данный феномен является следствием применения эвристических механизмов чистки конфликтных баз, которые реализованы во всех современных SAT-решателях, основанных на алгоритме CDCL (Conflict Driven Clause Learning). Описана новая техника, которая позволяет отслеживать повторно порождаемые дизъюнкты и запрещать их последующее удаление. На базе предложенных технических решений построен новый многопоточный SAT-решатель (SAT, SATisfiability), который на ряде SAT-задач, кодирующих обращение криптографических хеш-функций, существенно превзошел по эффективности многопоточные решатели, занимавшие в последние годы высокие места на специализированных соревнованиях. A phenomenon of conflict clauses generated repeatedly by SAT solvers is studied. Such clauses may appear during solving hard Boolean satisfiability problems (SAT). This phenomenon is caused by the fact that the modern SAT solvers are based on the CDCL algorithm that generates conflict clauses. A database of such clauses is periodically and partially cleaned. A new approach for practical SAT solving is proposed. According to this approach, the repeatedly generated conflict clauses are tracked, whereas their further generation is prohibited. Based on this approach, a multithreaded SAT solver was developed. This solver was compared with the best multithreaded SAT solvers awarded during the last SAT competitions. According to the experimental results, the developed solver greatly outperforms its competitors on several SAT instances encoding the inversion of some cryptographic hash functions.

Sign in / Sign up

Export Citation Format

Share Document