1 /*
2 * SAT4J: a SATisfiability library for Java Copyright (C) 2004-2006 Daniel Le Berre
3 *
4 * Based on the original minisat specification from:
5 *
6 * An extensible SAT solver. Niklas E?n and Niklas S?rensson. Proceedings of the
7 * Sixth International Conference on Theory and Applications of Satisfiability
8 * Testing, LNCS 2919, pp 502-518, 2003.
9 *
10 * This library is free software; you can redistribute it and/or modify it under
11 * the terms of the GNU Lesser General Public License as published by the Free
12 * Software Foundation; either version 2.1 of the License, or (at your option)
13 * any later version.
14 *
15 * This library is distributed in the hope that it will be useful, but WITHOUT
16 * ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
17 * FOR A PARTICULAR PURPOSE. See the GNU Lesser General Public License for more
18 * details.
19 *
20 * You should have received a copy of the GNU Lesser General Public License
21 * along with this library; if not, write to the Free Software Foundation, Inc.,
22 * 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
23 *
24 */
25
26 package org.sat4j.minisat.orders;
27
28 import org.sat4j.minisat.core.ILits;
29
30 /**
31 * @author leberre TODO To change the template for this generated type comment
32 * go to Window - Preferences - Java - Code Style - Code Templates
33 */
34 public class PureOrder extends VarOrder<ILits> {
35
36 /**
37 * Comment for <code>serialVersionUID</code>
38 */
39 private static final long serialVersionUID = 1L;
40
41 private int period;
42
43 private int cpt;
44
45 public PureOrder() {
46 this(20);
47 }
48
49 public PureOrder(int p) {
50 setPeriod(p);
51 }
52
53 public final void setPeriod(int p) {
54 period = p;
55 cpt = period;
56 }
57
58 public int getPeriod() {
59 return period;
60 }
61
62 /*
63 * (non-Javadoc)
64 *
65 * @see org.sat4j.minisat.core.VarOrder#select()
66 */
67 @Override
68 public int select() {
69 // wait period branching
70 if (cpt < period) {
71 cpt++;
72 } else {
73 // try to find a pure literal
74 cpt = 0;
75 int nblits = 2 * lits.nVars();
76 for (int i = 2; i <= nblits; i++) {
77 if (lits.isUnassigned(i) && lits.watches(i).size() > 0
78 && lits.watches(i ^ 1).size() == 0) {
79 return i;
80 }
81 }
82 }
83 // not found: using normal order
84 return super.select();
85 }
86
87 @Override
88 public String toString() {
89 return "tries to first branch on a single phase watched unassigned variable (pure literal if using a CB data structure) else VSIDS from MiniSAT"; //$NON-NLS-1$
90 }
91 }