View Javadoc

1   /*******************************************************************************
2   * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre
3   *
4   * All rights reserved. This program and the accompanying materials
5   * are made available under the terms of the Eclipse Public License v1.0
6   * which accompanies this distribution, and is available at
7   * http://www.eclipse.org/legal/epl-v10.html
8   *
9   * Alternatively, the contents of this file may be used under the terms of
10  * either the GNU Lesser General Public License Version 2.1 or later (the
11  * "LGPL"), in which case the provisions of the LGPL are applicable instead
12  * of those above. If you wish to allow use of your version of this file only
13  * under the terms of the LGPL, and not to allow others to use your version of
14  * this file under the terms of the EPL, indicate your decision by deleting
15  * the provisions above and replace them with the notice and other provisions
16  * required by the LGPL. If you do not delete the provisions above, a recipient
17  * may use your version of this file under the terms of the EPL or the LGPL.
18  * 
19  * Based on the original MiniSat specification from:
20  * 
21  * An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the
22  * Sixth International Conference on Theory and Applications of Satisfiability
23  * Testing, LNCS 2919, pp 502-518, 2003.
24  *
25  * See www.minisat.se for the original solver in C++.
26  * 
27  *******************************************************************************/
28  package org.sat4j.minisat.core;
29  
30  import java.io.Serializable;
31  import java.lang.reflect.Field;
32  
33  /**
34   * Some parameters used during the search.
35   * 
36   * @author daniel
37   * 
38   */
39  public class SearchParams implements Serializable {
40  
41      private static final long serialVersionUID = 1L;
42  
43      /**
44       * Default search parameters.
45       *
46       */
47      public SearchParams() {
48          this(0.95, 0.999, 1.5, 100);
49      }
50  
51      /** 
52       * 
53       * @param conflictBound the initial conflict bound for the first restart.
54       */
55      public SearchParams(int conflictBound) {
56          this(0.95, 0.999, 1.5, conflictBound);
57      }
58  
59      public SearchParams(double confincfactor, int conflictBound) {
60          this(0.95, 0.999, confincfactor, conflictBound);
61      }
62  
63      /**
64       * @param d
65       *            variable decay
66       * @param e
67       *            clause decay
68       * @param f
69       *            conflict bound increase factor
70       * @param i
71       *            initialConflictBound
72       */
73      public SearchParams(double d, double e, double f, int i) {
74          varDecay = d;
75          claDecay = e;
76          conflictBoundIncFactor = f;
77          initConflictBound = i;
78      }
79  
80      /**
81       * @return la valeur de clause decay
82       */
83      public double getClaDecay() {
84          return claDecay;
85      }
86  
87      /**
88       * @return la valeur de var decay
89       */
90      public double getVarDecay() {
91          return varDecay;
92      }
93  
94      private double claDecay;
95  
96      private double varDecay;
97  
98      private double conflictBoundIncFactor;
99  
100     private int initConflictBound;
101 
102     /*
103      * (non-Javadoc)
104      * 
105      * @see java.lang.Object#toString()
106      */
107     @Override
108     public String toString() {
109         StringBuffer stb = new StringBuffer();
110         for (Field field : SearchParams.class.getDeclaredFields()) {
111             if (!field.getName().startsWith("serial")&&!field.getName().startsWith("class")) {
112                 stb.append(field.getName());
113                 stb.append("="); //$NON-NLS-1$
114                 try {
115                     stb.append(field.get(this));
116                 } catch (IllegalArgumentException e) {
117                     e.printStackTrace();
118                 } catch (IllegalAccessException e) {
119                     e.printStackTrace();
120                 }
121                 stb.append(" "); //$NON-NLS-1$
122             }
123         }
124         return stb.toString();
125     }
126 
127     /**
128      * @param conflictBoundIncFactor
129      *            the conflictBoundIncFactor to set
130      */
131     public void setConflictBoundIncFactor(double conflictBoundIncFactor) {
132         this.conflictBoundIncFactor = conflictBoundIncFactor;
133     }
134 
135     /**
136      * @param initConflictBound
137      *            the initConflictBound to set
138      */
139     public void setInitConflictBound(int initConflictBound) {
140         this.initConflictBound = initConflictBound;
141     }
142 
143     /**
144      * @return the conflictBoundIncFactor
145      */
146     public double getConflictBoundIncFactor() {
147         return conflictBoundIncFactor;
148     }
149 
150     /**
151      * @return the initConflictBound
152      */
153     public int getInitConflictBound() {
154         return initConflictBound;
155     }
156 
157     /**
158      * @param claDecay
159      *            the claDecay to set
160      */
161     public void setClaDecay(double claDecay) {
162         this.claDecay = claDecay;
163     }
164 
165     /**
166      * @param varDecay
167      *            the varDecay to set
168      */
169     public void setVarDecay(double varDecay) {
170         this.varDecay = varDecay;
171     }
172 }