Toward A Good Algorithm for Determining Unsatisfiability of Propositional Formulas,

Abstract

We present progress toward an algorithm that provides short certificates of unsatisfiability with high probability when inputs are random instances of 3-SAT. Such an algorithm would incorporate an approximation algorithm A for the 3-Hitting Set problem. Using A it would determine an approximation for the minimum fraction of variables that must be set to true (false) in order to satisfy the positive (negative) clauses. If the fraction is high enough, then the instance is deemed unsatisfiable.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
May 20, 1997
Accession Number
ADA325940

Entities

People

  • John Franco
  • R. Swaminathan

Organizations

  • University of Cincinnati

Tags

DTIC Thesaurus Topics

  • Algorithms
  • Binomials
  • Computer Science
  • Computers
  • Equations
  • Guarantees
  • Iterations
  • Military Research
  • Optimization
  • Polynomials
  • Probability
  • Universities

Fields of Study

  • Computer science

Readers

  • Educational Psychology
  • Operations Research
  • Wetland-Land-Environmental Management.