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

From: Thomas A. Li (tli_at_corporola.com)
Date: 01/26/05 

Date: Wed, 26 Jan 2005 09:25:59 -0500

What is "Extended resolution"? Please give a definition or source of
definition.

Thomas Li

"Will Nayor" <pub@willnaylor.com> wrote in message
news:10veflhfkatig29@corp.supernews.com...
> 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