Follow us on Twitter
Lab of Misfits

This is part of the Robotsprogramme



Reducing SAT algorithms

The Constraint Satisfaction Problem (CSP) is one of the most prominent problems in artificial intelligence, logic, theoretical computer science, engineering and many other areas in science and industry. One instance of a CSP, the satisfiability problem in propositional logic (SAT), has become increasingly popular and has illuminated important insights into our understanding of the fundamentals of computation. Though the concept of representing propositional formulae as n-partite graphs is certainly not novel, in this paper we introduce a new polynomial reduction from 3SAT to Gn7 graphs and demonstrate that this framework has advantages over the standard representation. More specifically, after presenting the reduction we show that many hard 3SAT instances represented in this framework can be solved using a basic arc-consistency algorithm, and finally we discuss the potential advantages and implications of using such a representation.

Reducing SAT algorithms

Download paper

A New Reduction from SAT to n-Partite Graphs.
Download pdf