Comparing Techniques for Proving Unsatisfiability

Abstract

We compare two standard techniques for satisfiability (SAT), which are basic for verification of microprocessor systems. We propose an approach for construction of shorter resolution refutations based on a standard approach called DPLL.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 2002
Accession Number
ADP013964

Entities

People

  • Hans Zantema
  • Olga Tveretina

Tags

DTIC Thesaurus Topics

  • Algorithms
  • Circuits
  • Computer Science
  • Computers
  • Construction
  • Digital Circuits
  • Electromagnetism
  • Microprocessors
  • Specifications
  • Standards
  • Technical Information Centers
  • Verification

Fields of Study

  • Computer science
  • Mathematics

Readers

  • Mathematical Modeling and Probability Theory.
  • Parallel and Distributed Computing.