APPLICATION OF INCREMENTAL SATISFIABILITY PROBLEM SOLVERS FOR NON-DETERMINISTIC POLYNOMIAL-TIME HARD PROBLEMS AS ILLUSTRATED BY MINIMAL BOOLEAN FORMULA SYNTHESIS PROBLEM

APPLICATION OF INCREMENTAL SATISFIABILITY PROBLEM SOLVERS FOR NON-DETERMINISTIC POLYNOMIAL-TIME HARD PROBLEMS AS ILLUSTRATED BY MINIMAL BOOLEAN FORMULA SYNTHESIS PROBLEM

Subject of Research. The paper considers a method for solution of the nondeterministic polynomial hard problem (NP-hard problem) of a minimal Boolean formula synthesis from a given truth table. The solution of this problem is proposed based on its reduction to the Boolean satisfiability problem (SAT...

Full description

Bibliographic Details
Main Author: Konstantin I. Chukharev
Format: Article
Language:English
Published: Saint Petersburg National Research University of Information Technologies, Mechanics and Optics (ITMO University) 2020-12-01
Series:Naučno-tehničeskij Vestnik Informacionnyh Tehnologij, Mehaniki i Optiki
Subjects:
satisfiability problem (sat)
incremental satisfiability problem (sat) solvers
non-deterministic polynomial-time (np) hard problems
constraint programming
boolean formula synthesis
tseytin transformations
symmetry breaking
kotlin
framework
java native interface
Online Access:https://ntv.ifmo.ru/file/article/20008.pdf

Internet

https://ntv.ifmo.ru/file/article/20008.pdf

Similar Items