Combining SAT Methods with Non-Clausal Decision Heuristics | Zendy

Clark Barrett | Zendy; Jacob Donham | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Combining SAT Methods with Non-Clausal Decision Heuristics

Author(s) -

Clark Barrett,

Jacob Donham

Publication year - 2005

Publication title -

electronic notes in theoretical computer science

Language(s) - English

Resource type - Journals

SCImago Journal Rank - 0.242

H-Index - 60

ISSN - 1571-0661

DOI - 10.1016/j.entcs.2004.09.042

Subject(s) - heuristics , computer science , maximum satisfiability problem , propositional formula , conjunctive normal form , propositional calculus , boolean function , order (exchange) , algorithm , theoretical computer science , propositional variable , mathematics , artificial intelligence , mathematical optimization , programming language , finance , intermediate logic , economics , description logic

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

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research