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

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

Date: Wed, 26 Jan 2005 18:19:49 -0800

That is the question I am asking the newsgroups.

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

Loading