Logic Programming with Satisfiability

TL;DR

This paper introduces a Prolog interface to the MiniSat SAT solver, combining logic programming and satisfiability solving to efficiently encode and solve complex search problems, exemplified by Partial MAXSAT.

Contribution

It presents a novel integration of Prolog with SAT solving, enabling logic programming to leverage efficient SAT solvers for problem encoding and solving.

Findings

Prolog interface to MiniSat enhances problem-solving capabilities.

Demonstrated solving of Partial MAXSAT instances.

Shows synergy between logic programming and SAT solving.

Abstract

This paper presents a Prolog interface to the MiniSat satisfiability solver. Logic program- ming with satisfiability combines the strengths of the two paradigms: logic programming for encoding search problems into satisfiability on the one hand and efficient SAT solving on the other. This synergy between these two exposes a programming paradigm which we propose here as a logic programming pearl. To illustrate logic programming with SAT solving we give an example Prolog program which solves instances of Partial MAXSAT.