Toward A Good Algorithm for Determining Unsatisfiability of PropositionalFormulas

摘要

We present progress toward an algorithm that provides short certificates ofunsatisfiability 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.