Q: solving SAT: generating extended resolution proofs using techniques for resolution?

From: Will Nayor (pub_at_willnaylor.com)
Date: 01/26/05 

Date: Tue, 25 Jan 2005 22:53:23 -0800

The most successful techniques for solving SAT to date
work by searching for resolution refutations [1], [2], [3]. It is well
known that resolution refutations are exponential length
for some rather trivial problems (pigeon-hole, reordering XOR,
reordering addition, etc).

Extended resolution is resolution allowing definition
of new boolean variables. There are no problems in NP which
are known to require exponential length extended resolution
refutations (or at least, I do not know of any).
So I have been trying to find a way to extend the techniques
which work so well at finding short resolution refutations to find
short extended resolution refutation.

I would appreciate it if people could post advice for me
or references or results which might be helpful to my
quest.

References:

[1] Joao Silva, Karem Sakallah: GRASP - A New Search Algorithm for
Satisfiability,
      1996 ICCAD proceedings

[2] Matthew Moskewicz, Conor Madigan, et al: Chaff - Engineering an
      Efficient SAT Solver

[3] Evgueni Goldberg, Yakov Novikov: BerkMin: a Fast and Robust Sat-Solver

  - Will Naylor
    email: pub@willnaylor.com

Relevant Pages