Quantum computers promise to allow for great improvements in the solution of ｋ-SAT problem, determining whether a set of clauses with ｋ variables have a satisfiable boolean assignment, which is one of the fundamental problems of computational logic. Given the recent advancements of quantum computers, we argue that they allow for great improvements in solving the ｋ-SAT problem. In order to evaluate this possibility, in this work, we generalized a pre-existing quantum 3-SAT solver [1] to the most general case for the number of variables, clauses, and ｋ, using the IBM Qiskit library [2]. We extended basic gates and steps of the underlying algorithm to reduce the number of used qubits and gates, in order to deal with the decoherence problem [3]. We tested our solution on complex instances of ｋ-SAT, which preserved the exponential speedup promised by Grover algorithm [4].
Generalizing an exactly-1 SAT solver for arbitrary numbers of variables, clauses, and K
Di Nitto E.
2020-01-01
Abstract
Quantum computers promise to allow for great improvements in the solution of ｋ-SAT problem, determining whether a set of clauses with ｋ variables have a satisfiable boolean assignment, which is one of the fundamental problems of computational logic. Given the recent advancements of quantum computers, we argue that they allow for great improvements in solving the ｋ-SAT problem. In order to evaluate this possibility, in this work, we generalized a pre-existing quantum 3-SAT solver [1] to the most general case for the number of variables, clauses, and ｋ, using the IBM Qiskit library [2]. We extended basic gates and steps of the underlying algorithm to reduce the number of used qubits and gates, in order to deal with the decoherence problem [3]. We tested our solution on complex instances of ｋ-SAT, which preserved the exponential speedup promised by Grover algorithm [4].I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
