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

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

Date: Wed, 26 Jan 2005 09:00:54 -0800

As my post states, "extended resolution" is resolution,
but also allowing definition of a new boolean variable at
any point in the proof. The definition of the new variable
must not add any new information or restriction to the system.

For example:

Suppose your SAT problem contains the clauses
   (A or !B or C)
   (B or D or E)

Resolving on variable B implies the new clause
   (A or C or D or E)

A "resolution proof" or "resolution refutation"
is a sequence of such resolution steps that results
in proving the empty clause.

Extended resolution allows the additional step of
introducing a new boolean variable at any time.
For example, I could add NEWVAR == A exclusive_or B,
which in the language of SATISFIABILITY problem is
these 4 clauses:
   (A or B or !NEWVAR)
   (A or !B or NEWVAR)
   (!A or B or NEWVAR)
   (!A or !B or !NEWVAR)

Resolution is weak in sense that many simple
theorems that are easy to prove by other methods
require proofs of exponential length in resolution.
However, extended resolution can simulate most or
all other methods of proof, and hence extended
resolution has short proves for most or all theorems
that have short proofs in other systems.

Thomas A. Li wrote:
> 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