Combining SAT Methods with Non-Clausal Decision Heuristics

Clark Barrett, Jacob Donham

Research output: Contribution to journalArticle

Abstract

A decision procedure for arbitrary first-order formulas can be viewed as combining a propositional search with a decision procedure for conjunctions of first-order literals, so Boolean SAT methods can be used for the propositional search in order to improve the performance of the overall decision procedure. We show how to combine some Boolean SAT methods with non-clausal heuristics developed for first-order decision procedures. The combination of methods leads to a smaller number of decisions than either method alone.

Original languageEnglish (US)
Pages (from-to)3-12
Number of pages10
JournalElectronic Notes in Theoretical Computer Science
Volume125
Issue number3
DOIs
StatePublished - Jul 18 2005

Fingerprint

Decision Procedures
Heuristics
First-order
Arbitrary

Keywords

  • Boolean satisfiability
  • CVC Lite
  • Decision heuristics
  • Non-clausal
  • Satisfiability modulo theories

ASJC Scopus subject areas

  • Computer Science (miscellaneous)

Cite this

Combining SAT Methods with Non-Clausal Decision Heuristics. / Barrett, Clark; Donham, Jacob.

In: Electronic Notes in Theoretical Computer Science, Vol. 125, No. 3, 18.07.2005, p. 3-12.

Research output: Contribution to journalArticle

Barrett, Clark ; Donham, Jacob. / Combining SAT Methods with Non-Clausal Decision Heuristics. In: Electronic Notes in Theoretical Computer Science. 2005 ; Vol. 125, No. 3. pp. 3-12.
@article{494514093d2e455c946b5db0fee6a6d0,
title = "Combining SAT Methods with Non-Clausal Decision Heuristics",
abstract = "A decision procedure for arbitrary first-order formulas can be viewed as combining a propositional search with a decision procedure for conjunctions of first-order literals, so Boolean SAT methods can be used for the propositional search in order to improve the performance of the overall decision procedure. We show how to combine some Boolean SAT methods with non-clausal heuristics developed for first-order decision procedures. The combination of methods leads to a smaller number of decisions than either method alone.",
keywords = "Boolean satisfiability, CVC Lite, Decision heuristics, Non-clausal, Satisfiability modulo theories",
author = "Clark Barrett and Jacob Donham",
year = "2005",
month = "7",
day = "18",
doi = "10.1016/j.entcs.2004.09.042",
language = "English (US)",
volume = "125",
pages = "3--12",
journal = "Electronic Notes in Theoretical Computer Science",
issn = "1571-0661",
publisher = "Elsevier",
number = "3",

}

TY - JOUR

T1 - Combining SAT Methods with Non-Clausal Decision Heuristics

AU - Barrett, Clark

AU - Donham, Jacob

PY - 2005/7/18

Y1 - 2005/7/18

N2 - A decision procedure for arbitrary first-order formulas can be viewed as combining a propositional search with a decision procedure for conjunctions of first-order literals, so Boolean SAT methods can be used for the propositional search in order to improve the performance of the overall decision procedure. We show how to combine some Boolean SAT methods with non-clausal heuristics developed for first-order decision procedures. The combination of methods leads to a smaller number of decisions than either method alone.

AB - A decision procedure for arbitrary first-order formulas can be viewed as combining a propositional search with a decision procedure for conjunctions of first-order literals, so Boolean SAT methods can be used for the propositional search in order to improve the performance of the overall decision procedure. We show how to combine some Boolean SAT methods with non-clausal heuristics developed for first-order decision procedures. The combination of methods leads to a smaller number of decisions than either method alone.

KW - Boolean satisfiability

KW - CVC Lite

KW - Decision heuristics

KW - Non-clausal

KW - Satisfiability modulo theories

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

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

U2 - 10.1016/j.entcs.2004.09.042

DO - 10.1016/j.entcs.2004.09.042

M3 - Article

VL - 125

SP - 3

EP - 12

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

SN - 1571-0661

IS - 3

ER -