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

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

  • Next message: simon.plouffe_at_sympatico.ca: "2 maple important bugs, ifactor(10000!);pi(500000000);" 
    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
    >>>
    >>>
    >>>
    >>
    >
    >

  • Next message: simon.plouffe_at_sympatico.ca: "2 maple important bugs, ifactor(10000!);pi(500000000);"

    Relevant Pages

    • Re: solving SAT: generating extended resolution proofs using techniques for resolution?
      ... >>is a sequence of such resolution steps that results ... >>in proving the empty clause. ... >>resolution has short proves for most or all theorems ...
      (comp.theory)
    • Termination of resolution
      ... check clauses generated by resolution so that resolving this KB does not ... I know that resolution is undecidable in general (because it is a proof procedure for first order logic, whose proofs are undecidable), but the way this resolution diverges seems to me to be possible to catch with some kind of pattern matching. ... This is not a theoretical example, either: the above clause is effectively a statement that the predicate p is transitive... ...
      (sci.logic)
    • Re: Termination of resolution
      ... I tried a little bit googling around, but actually I don't understand why it is okay to factorise the clauses: ... binary resolution rule is used only. ... again a tautological clause and the rule wouldn't ...
      (sci.logic)
    • Re: Termination of resolution
      ... Panu Kalliokoski schrieb: ... I know that resolution is undecidable in general, but the way this resolution diverges seems to me to be possible to catch with some kind of pattern matching. ... This is not a theoretical example, either: the above clause is effectively a statement that the predicate p is transitive... ... again a tautological clause and the rule wouldn't ...
      (sci.logic)
    • Re: solving SAT: generating extended resolution proofs using techniques for resolution?
      ... As my post states, "extended resolution" is resolution, ... For example, I could add NEWVAR == A exclusive_or B, ... >>of new boolean variables. ...
      (comp.theory)