Checking satisfiability of first-order formulas by incremental translation to SAT

Clark W. Barrett, David L. Dill, Aaron Stump

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

In the past few years, general-purpose propositional satisfiability (SAT) solvers have improved dramatically in performance and have been used to tackle many new problems.It has also been shown that certain simple fragments of first-order logic can be decided efficiently by first translating the problem into an equivalent SAT problem and then using a fast SAT solver.In this paper, we describe an alternative but similar approach to using SAT in conjunction with a more expressive fragment of first-order logic.H owever, rather than translating the entire formula up front, the formula is incrementally translated during a search for the solution.A s a result, only that portion of the translation that is actually relevant to the solution is obtained.We describe a number of obstacles that had to be overcome before developing an approach which was ultimately very effective, and give results on verification benchmarks using CVC (Cooperating Validity Checker), which includes the Chaff SAT solver.Th e results show a performance gain of several orders of magnitude over CVC without Chaff and indicate that the method is more robust than the heuristics found in CVC’s predecessor, SVC.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 14th International Conference, CAV 2002, Proceedings
PublisherSpringer Verlag
Pages236-249
Number of pages14
Volume2404
ISBN (Print)9783540439974
StatePublished - 2002
Event14th International Conference on Computer Aided Verification, CAV 2002 - Copenhagen, Denmark
Duration: Jul 27 2002Jul 31 2002

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2404
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other14th International Conference on Computer Aided Verification, CAV 2002
CountryDenmark
CityCopenhagen
Period7/27/027/31/02

Fingerprint

First-order Logic
First-order
Fragment
Satisfiability Problem
Entire
Heuristics
Benchmark
Alternatives

Keywords

  • Decision Procedures
  • First-Order Logic
  • Propositional Satisfiability
  • Satisfiability

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Barrett, C. W., Dill, D. L., & Stump, A. (2002). Checking satisfiability of first-order formulas by incremental translation to SAT. In Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings (Vol. 2404, pp. 236-249). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2404). Springer Verlag.

Checking satisfiability of first-order formulas by incremental translation to SAT. / Barrett, Clark W.; Dill, David L.; Stump, Aaron.

Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings. Vol. 2404 Springer Verlag, 2002. p. 236-249 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2404).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Barrett, CW, Dill, DL & Stump, A 2002, Checking satisfiability of first-order formulas by incremental translation to SAT. in Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings. vol. 2404, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2404, Springer Verlag, pp. 236-249, 14th International Conference on Computer Aided Verification, CAV 2002, Copenhagen, Denmark, 7/27/02.
Barrett CW, Dill DL, Stump A. Checking satisfiability of first-order formulas by incremental translation to SAT. In Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings. Vol. 2404. Springer Verlag. 2002. p. 236-249. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Barrett, Clark W. ; Dill, David L. ; Stump, Aaron. / Checking satisfiability of first-order formulas by incremental translation to SAT. Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings. Vol. 2404 Springer Verlag, 2002. pp. 236-249 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{3471313934d44e21bc1bc8499a891d66,
title = "Checking satisfiability of first-order formulas by incremental translation to SAT",
abstract = "In the past few years, general-purpose propositional satisfiability (SAT) solvers have improved dramatically in performance and have been used to tackle many new problems.It has also been shown that certain simple fragments of first-order logic can be decided efficiently by first translating the problem into an equivalent SAT problem and then using a fast SAT solver.In this paper, we describe an alternative but similar approach to using SAT in conjunction with a more expressive fragment of first-order logic.H owever, rather than translating the entire formula up front, the formula is incrementally translated during a search for the solution.A s a result, only that portion of the translation that is actually relevant to the solution is obtained.We describe a number of obstacles that had to be overcome before developing an approach which was ultimately very effective, and give results on verification benchmarks using CVC (Cooperating Validity Checker), which includes the Chaff SAT solver.Th e results show a performance gain of several orders of magnitude over CVC without Chaff and indicate that the method is more robust than the heuristics found in CVC’s predecessor, SVC.",
keywords = "Decision Procedures, First-Order Logic, Propositional Satisfiability, Satisfiability",
author = "Barrett, {Clark W.} and Dill, {David L.} and Aaron Stump",
year = "2002",
language = "English (US)",
isbn = "9783540439974",
volume = "2404",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "236--249",
booktitle = "Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings",

}

TY - GEN

T1 - Checking satisfiability of first-order formulas by incremental translation to SAT

AU - Barrett, Clark W.

AU - Dill, David L.

AU - Stump, Aaron

PY - 2002

Y1 - 2002

N2 - In the past few years, general-purpose propositional satisfiability (SAT) solvers have improved dramatically in performance and have been used to tackle many new problems.It has also been shown that certain simple fragments of first-order logic can be decided efficiently by first translating the problem into an equivalent SAT problem and then using a fast SAT solver.In this paper, we describe an alternative but similar approach to using SAT in conjunction with a more expressive fragment of first-order logic.H owever, rather than translating the entire formula up front, the formula is incrementally translated during a search for the solution.A s a result, only that portion of the translation that is actually relevant to the solution is obtained.We describe a number of obstacles that had to be overcome before developing an approach which was ultimately very effective, and give results on verification benchmarks using CVC (Cooperating Validity Checker), which includes the Chaff SAT solver.Th e results show a performance gain of several orders of magnitude over CVC without Chaff and indicate that the method is more robust than the heuristics found in CVC’s predecessor, SVC.

AB - In the past few years, general-purpose propositional satisfiability (SAT) solvers have improved dramatically in performance and have been used to tackle many new problems.It has also been shown that certain simple fragments of first-order logic can be decided efficiently by first translating the problem into an equivalent SAT problem and then using a fast SAT solver.In this paper, we describe an alternative but similar approach to using SAT in conjunction with a more expressive fragment of first-order logic.H owever, rather than translating the entire formula up front, the formula is incrementally translated during a search for the solution.A s a result, only that portion of the translation that is actually relevant to the solution is obtained.We describe a number of obstacles that had to be overcome before developing an approach which was ultimately very effective, and give results on verification benchmarks using CVC (Cooperating Validity Checker), which includes the Chaff SAT solver.Th e results show a performance gain of several orders of magnitude over CVC without Chaff and indicate that the method is more robust than the heuristics found in CVC’s predecessor, SVC.

KW - Decision Procedures

KW - First-Order Logic

KW - Propositional Satisfiability

KW - Satisfiability

UR - http://www.scopus.com/inward/record.url?scp=84937569311&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84937569311&partnerID=8YFLogxK

M3 - Conference contribution

SN - 9783540439974

VL - 2404

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 236

EP - 249

BT - Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings

PB - Springer Verlag

ER -