Combining SAT Methods with Non-Clausal Decision Heuristics

Clark Barrett; Jacob Donham

doi:10.1016/j.entcs.2004.09.042

Combining SAT Methods with Non-Clausal Decision Heuristics

Clark Barrett, Jacob Donham

Computer Science

Research output: Contribution to journal › Conference article › peer-review

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 language	English (US)
Pages (from-to)	3-12
Number of pages	10
Journal	Electronic Notes in Theoretical Computer Science
Volume	125
Issue number	3
DOIs	https://doi.org/10.1016/j.entcs.2004.09.042
State	Published - Jul 18 2005

Keywords

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

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1016/j.entcs.2004.09.042

Cite this

@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",

note = "Funding Information: 1 This research was supported by a grant from Intel Corporation. does not necessarily reflect the position or the policy of Intel. 2 Email: [email protected] 3 Email: [email protected]",

year = "2005",

month = jul,

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 B.V.",

number = "3",

}

TY - JOUR

T1 - Combining SAT Methods with Non-Clausal Decision Heuristics

AU - Barrett, Clark

AU - Donham, Jacob

N1 - Funding Information: 1 This research was supported by a grant from Intel Corporation. does not necessarily reflect the position or the policy of Intel. 2 Email: [email protected] 3 Email: [email protected]

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 - Conference article

AN - SCOPUS:21644479967

SN - 1571-0661

VL - 125

SP - 3

EP - 12

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

IS - 3

ER -

Combining SAT Methods with Non-Clausal Decision Heuristics

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this