solving SAT: generating extended resolution proofs using techniques for resolution

From: Will Naylor (wcncom_at_aol.com)
Date: 11/13/04

  • Next message: Yong Zhang: "What is the rank of CS theory conferences?" 
    Date: 13 Nov 2004 04:51:28 GMT

    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 (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: Yong Zhang: "What is the rank of CS theory conferences?"

    Relevant Pages