Quantum tunneling and quantum walks as algorithmic resources to solve hard K-SAT instances

We present a new quantum heuristic algorithm aimed at finding satisfying assignments for hard K-SAT instances using a continuous time quantum walk that explicitly exploits the properties of quantum tunneling. Our algorithm uses a Hamiltonian $$H_A(F)$$ H A ( F ) which is specifically constructed to solve a K-SAT instance F. The heuristic algorithm aims at iteratively reducing the Hamming distance between an evolving state $${|{\psi _j}\rangle }$$ | ψ j ⟩ and a state that represents a satisfying assignment for F. Each iteration consists on the evolution of $${|{\psi _j}\rangle }$$ | ψ j ⟩ (where j is the iteration number) under $$e^{-iH_At}$$ e - i H A t , a measurement that collapses the superposition, a check to see if the post-measurement state satisfies F and in the case it does not, an update to $$H_A$$ H A for the next iteration. Operator $$H_A$$ H A describes a continuous time quantum walk over a hypercube graph with potential barriers that makes an evolving state to scatter and mostly follow the shortest tunneling paths with the smaller potentials that lead to a state $${|{s}\rangle }$$ | s ⟩ that represents a satisfying assignment for F. The potential barriers in the Hamiltonian $$H_A$$ H A are constructed through a process that does not require any previous knowledge on the satisfying assignments for the instance F. Due to the topology of $$H_A$$ H A each iteration is expected to reduce the Hamming distance between each post measurement state and a state $${|{s}\rangle }$$ | s ⟩ . If the state $${|{s}\rangle }$$ | s ⟩ is not measured after n iterations (the number n of logical variables in the instance F being solved), the algorithm is restarted. Periodic measurements and quantum tunneling also give the possibility of getting out of local minima. Our numerical simulations show a success rate of 0.66 on measuring $${|{s}\rangle }$$ | s ⟩ on the first run of the algorithm (i.e., without restarting after n iterations) on thousands of 3-SAT instances of 4, 6, and 10 variables with unique satisfying assignments.

On Super Strong ETH

Multiple known algorithmic paradigms (backtracking, local search and the polynomial method) only yield a 2n(1-1/O(k)) time algorithm for k-SAT in the worst case. For this reason, it has been hypothesized that the worst-case k-SAT problem cannot be solved in 2n(1-f(k)/k) time for any unbounded function f. This hypothesis has been called the "Super-Strong ETH", modelled after the ETH and the Strong ETH. It has also been hypothesized that k-SAT is hard to solve for randomly chosen instances near the "critical threshold", where the clause-to-variable ratio is such that randomly chosen instances are satisfiable with probability 1/2. We give a randomized algorithm which refutes the Super-Strong ETH for the case of random k-SAT and planted k-SAT for any clause-to-variable ratio. For example, given any random k-SAT instance F with n variables and m clauses, our algorithm decides satisfiability for F in 2n(1-c*log(k)/k) time with high probability (over the choice of the formula and the randomness of the algorithm). It turns out that a well-known algorithm from the literature on SAT algorithms does the job: the PPZ algorithm of Paturi, Pudlak, and Zane (1999). The Unique k-SAT problem is the special case where there is at most one satisfying assignment. Improving prior reductions, we show that the Super-Strong ETHs for Unique k-SAT and k-SAT are equivalent. More precisely, we show the time complexities of Unique k-SAT and k-SAT are very tightly correlated: if Unique k-SAT is in 2n(1-f(k)/k) time for an unbounded f, then k-SAT is in 2n(1-f(k)/(2k)) time.

NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability

In this paper, we analyze Boolean formulas in conjunctive normal form (CNF) from the perspective of read-once resolution (ROR) refutation schemes. A read-once (resolution) refutation is one in which each clause is used at most once. Derived clauses can be used as many times as they are deduced. However, clauses in the original formula can only be used as part of one derivation. It is well known that ROR is not complete; that is, there exist unsatisfiable formulas for which no ROR exists. Likewise, the problem of checking if a 3CNF formula has a read-once refutation is NP-complete. This paper is concerned with a variant of satisfiability called not-all-equal satisfiability (NAE-satisfiability). A CNF formula is NAE-satisfiable if it has a satisfying assignment in which at least one literal in each clause is set to false. It is well known that the problem of checking NAE-satisfiability is NP-complete. Clearly, the class of CNF formulas which are NAE-satisfiable is a proper subset of satisfiable CNF formulas. It follows that traditional resolution cannot always find a proof of NAE-unsatisfiability. Thus, traditional resolution is not a sound procedure for checking NAE-satisfiability. In this paper, we introduce a variant of resolution called NAE-resolution which is a sound and complete procedure for checking NAE-satisfiability in CNF formulas. The focus of this paper is on a variant of NAE-resolution called read-once NAE-resolution in which each clause (input or derived) can be part of at most one NAE-resolution step. Our principal result is that read-once NAE-resolution is a sound and complete procedure for 2CNF formulas. Furthermore, we provide an algorithm to determine the smallest such NAE-resolution in polynomial time. This is in stark contrast to the corresponding problem concerning 2CNF formulas and ROR refutations. We also show that the problem of checking whether a 3CNF formula has a read-once NAE-resolution is NP-complete.

(1,0)-Super Solutions of (k,s)-CNF Formula

A (1,0)-super solution is a satisfying assignment such that if the value of any one variable is flipped to the opposite value, the new assignment is still a satisfying assignment. Namely, every clause must contain at least two satisfied literals. Because of its robustness, super solutions are concerned in combinatorial optimization problems and decision problems. In this paper, we investigate the existence conditions of the (1,0)-super solution of ( k , s ) -CNF formula, and give a reduction method that transform from k-SAT to (1,0)- ( k + 1 , s ) -SAT if there is a ( k + 1 , s )-CNF formula without a (1,0)-super solution. Here, ( k , s ) -CNF is a subclass of CNF in which each clause has exactly k distinct literals, and each variable occurs at most s times. (1,0)- ( k , s ) -SAT is a problem to decide whether a ( k , s ) -CNF formula has a (1,0)-super solution. We prove that for k > 3 , if there exists a ( k , s ) -CNF formula without a (1,0)-super solution, (1,0)- ( k , s ) -SAT is NP-complete. We show that for k > 3 , there is a critical function φ ( k ) such that every ( k , s ) -CNF formula has a (1,0)-super solution for s ≤ φ ( k ) and (1,0)- ( k , s ) -SAT is NP-complete for s > φ ( k ) . We further show some properties of the critical function φ ( k ) .

Evolving Solutions to Community-Structured Satisfiability Formulas

We study the ability of a simple mutation-only evolutionary algorithm to solve propositional satisfiability formulas with inherent community structure. We show that the community structure translates to good fitness-distance correlation properties, which implies that the objective function provides a strong signal in the search space for evolutionary algorithms to locate a satisfying assignment efficiently. We prove that when the formula clusters into communities of size s ∈ ω(logn) ∩O(nε/(2ε+2)) for some constant 0

Finding small counterexamples for abstract rewriting properties

Rewriting notions like termination, normal forms and confluence can be described in an abstract way referring to rewriting only as a binary relation. Several theorems on rewriting, like Newman's lemma, can be proved in this abstract setting. For investigating possible generalizations of such theorems, it is fruitful to have counterexamples showing that particular generalizations do not hold. In this paper, we develop a technique to find such counterexamples fully automatically, and we describe our tool Carpa that follows this technique. The basic idea is to fix the number of objects of the abstract rewrite system, and to express the conditions and the negation of the conclusion in a satisfiability (SAT) formula, and then call a current SAT solver. In case the formula turns out to be satisfiable, the resulting satisfying assignment yields a counterexample to the encoded property. We give several examples of finite abstract rewrite systems having remarkable properties that are found in this way fully automatically.

Atomic distributions in crystal structures solved by Boolean satisfiability techniques

The atomic distribution in crystal structures becomes very complex if atoms are disordered and randomly distributed over positions not being fully occupied. Interatomic distances between neighboring atoms might be too close for simultaneous occupancies and thus are mutually exclusive. The distribution of atoms over crystallographic positions avoiding close contacts with neighboring atoms represents an NP-complete problem that is believed to have no efficient solution. Here, we use Boolean satisfiability (SAT) techniques to find a valid atomic distribution pattern in the crystal structure. Distance constraints are encoded as conjunctions of logical disjunctions over Boolean variables and handed to a SAT solver. If a solution exists, the solver supplies a satisfying assignment to the Boolean variables yielding a valid distribution after decoding. That way the hitherto unsolved problem of distributing

A Multilevel Memetic Algorithm for Large SAT-Encoded Problems

Many researchers have focused on the satisfiability problem and on many of its variants due to its applicability in many areas of artificial intelligence. This NP-complete problem refers to the task of finding a satisfying assignment that makes a Boolean expression evaluate to True. In this work, we introduce a memetic algorithm that makes use of the multilevel paradigm. The multilevel paradigm refers to the process of dividing large and difficult problems into smaller ones, which are hopefully much easier to solve, and then work backward toward the solution of the original problem, using a solution from a previous level as a starting solution at the next level. Results comparing the memetic with and without the multilevel paradigm are presented using problem instances drawn from real industrial hardware designs.

An exact tensor network for the 3SAT problem

We construct a tensor network that delivers an unnormalized quantum state whose coefficients are the solutions to a given instance of 3SAT, an NP-complete problem. The tensor network contraction that corresponds to the norm of the state counts the number of solutions to the instance. It follows that exact contractions of this tensor network are in the \#P-complete computational complexity class, thus believed to be a hard task. Furthermore, we show that for a 3SAT instance with $n$ bits, it is enough to perform a polynomial number of contractions of the tensor network structure associated to the computation of local observables to obtain one of the explicit solutions to the problem, if any. Physical realization of a state described by a generic tensor network is equivalent to finding the satisfying assignment of a 3SAT instance and, consequently, this experimental task is expected to be hard.