Solving the Satisfiability Problem Through Boolean Networks

TL;DR

This paper introduces a novel method for solving SAT problems using boolean networks, establishing a correspondence between BN fixed points and SAT solutions, and proposing new algorithms that blend symbolic and connectionist approaches.

Contribution

The paper presents a new framework mapping SAT to boolean networks, enabling the development of innovative local search algorithms based on BN dynamics.

Findings

BN fixed points correspond to SAT solutions

New algorithms leverage BN dynamics for SAT solving

Framework integrates symbolic and connectionist computation

Abstract

In this paper we present a new approach to solve the satisfiability problem (SAT), based on boolean networks (BN). We define a mapping between a SAT instance and a BN, and we solve SAT problem by simulating the BN dynamics. We prove that BN fixed points correspond to the SAT solutions. The mapping presented allows to develop a new class of algorithms to solve SAT. Moreover, this new approach suggests new ways to combine symbolic and connectionist computation and provides a general framework for local search algorithms.