Resources
- The paper presentation will be available later
- Source code of Sathys
SatHyS (Sat Hybrid Solver) is a new
hybridization of local search and modern SAT solver. In our approach, both components
heavily cooperate through relevant information gathered during search. More precisely,
our hybrid solver alternatively performs the search process using local search and CDCL based SAT solvers. On the one hand,
at each node of the search tree, the local search component is used to extend to the
model, the current (consistent) partial assignment built by the CDCL based component.
On the other hand, the CDCL part is conditionally invoked by the local search compo-
nent when a local minima is encountered. Each solver benefits from the other in several
ways. First, each time a local minima is reached, the local search technique update the
activity of the boundary variables. The idea is to direct the CDCL search towards
boundary points proven to be important by Goldberg. Secondly, the polarities of
the literals involved in the best complete assignment found during local search are ex-
ploited by the CDCL component. From the other side, the CDCL solver shares with local
search the current partial assignment together with the learnt clauses. The originality of
our proposed hybrid SAT solver arises in alternating search of both components while
exchanging relevant information.
MinisatPsmDyn implements a new
dynamic management policy of the learnt clauses database. This framework is based on two important key points. First,
a new measure for identifying relevant learnt clauses based on the progress saving is proposed. The main advantage
of this measure, named PSM, is that it is dynamic and it
can be computed even if clauses does not participate in the search process (unlike the
VSIDS like measure). Second, a new learnt clauses database management framework is proposed.
It originally exploit a dynamic policy that activates the most promising learnt clauses while freezing irrelevant ones.
It contrasts with all the well-known deletion strategies, where a given learned clause is definitely eliminated.
(Source code )
Resources
- The paper and the presentation will be available later
- Source code of minisat-psm-dyn. This is a modified version of minisat 2.2 which embeds the dynamic managment of learnt clauses
- Here, you can find the 292 instances used in experiments. These instances come from the SAT'09 competition
- The graphics of figure 1 for all instances are here
- The graphics of figure 3 for all instances are here
- All scatter and cactus plots of the section 5 are here