Combining SAT Methods with Non-Clausal Decision Heuristics

Clark Barrett, Jacob Donham

Research output: Contribution to journalConference articlepeer-review


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
Issue number3
StatePublished - Jul 18 2005


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

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Combining SAT Methods with Non-Clausal Decision Heuristics'. Together they form a unique fingerprint.

Cite this