Re: question about GRASP/RELSAT stack management

From: Bart Demoen (bmd_at_cs.kuleuven.ac.be)
Date: 08/15/04 

Date: Sun, 15 Aug 2004 21:19:19 +0200

Wcncom wrote:

> Why do you think it is necessary to redo
> the 1,2,4,5 branches? Since new term is learned
> and new activity is recorded, isn't it likely that the
> algorithm will choose other variables to branch on
> (presumeably better ones)?

I was thinking about the case when 1,2,4,5 are independent of the
learned clause - but you are right that one can expect benefit from
using the new clause starting at an even older point in the tree.

Efficient Conflict Driven Learning in a Boolean Satisfiability Solver,
Lintao Zhang, Conor F. Madigan, Matthew H. Moskewicz, Sharad Malik.
mentions "random restarts". Is it related to what you propose ?

Cheers

Bart Demoen

Relevant Pages

  • Re: P = NP!
    ... on a public math forum, it seems his algorithm ... We start by, once again, referring to the DNF form even though we're explicitly told we're not trying to solve the DNF form. ... Oh, by the way, the algorithm is essentially "for all tokens in the expression, if one tcis true, then it's satisfiable." ... The first paragraph of the algorithm is easy enough to understand: go through the clauses from left to right, checking to see if each clause has a valid token. ...
    (sci.math)
  • Re: shootout
    ... Because the "algorithm" is supposed to be set for most ... benchmarks, perhaps some investigation is needed to ... In most implementations freeze is not very efficiently ... clause and some internal cut mechanism. ...
    (comp.lang.prolog)