Checking Satisfiability by Dependency Sequents

TL;DR

This paper presents DS-QSAT, a new algorithm for checking the satisfiability of CNF formulas using Dependency sequents, which improves scalability over traditional DPLL-based methods by focusing on proving satisfiability rather than finding explicit solutions.

Contribution

The paper introduces a novel D-sequent calculus and the DS-QSAT algorithm, extending SAT solving to the quantified case and surpassing DPLL limitations.

Findings

DS-QSAT outperforms DPLL in scalability.

D-sequents enable more efficient satisfiability proofs.

Experimental results validate the advantages of the new approach.

Abstract

We introduce a new algorithm for checking satisfiability based on a calculus of Dependency sequents (D-sequents). Given a CNF formula F(X), a D-sequent is a record stating that under a partial assignment a set of variables of X is redundant in formula \exists{X}[F]. The D-sequent calculus is based on operation join that forms a new D-sequent from two existing D-sequents. The new algorithm solves the quantified version of SAT. That is, given a satisfiable formula F, it, in general, does not produce an assignment satisfying F. The new algorithm is called DS-QSAT where DS stands for Dependency Sequent and Q for Quantified. Importantly, a DPLL-like procedure is only a special case of DS-QSAT where a very restricted kind of D-sequents is used. We argue that this restriction a) adversely affects scalability of SAT-solvers and b) is caused by looking for an explicit satisfying assignment rather than just proving satisfiability. We give experimental results substantiating these claims.