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

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

Date: Wed, 26 Jan 2005 19:58:03 -0500

Hi Will,

What is the procedure or the rule to add a new variable?
If you have a simple and deterministic algorithm to do so, it is marvelous.

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