2012/07/20 by Eugene Goldberg, Goldberg, Eugene, Panagiotis Manolios +1
Computer Science · #Discrete Mathematics (cs.DM) #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1207.5014
openalex publication_date 2012/07/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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 ∃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.