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 org.sat4j.specs.IConstr;
31  import org.sat4j.specs.IVecInt;
32  
33  /*
34   * Created on 16 oct. 2003
35   */
36  
37  /**
38   * Basic constraint abstraction used in Solver.
39   * 
40   * Any new constraint type should implement that interface.
41   * 
42   * @author leberre
43   */
44  public interface Constr extends Propagatable, IConstr {
45  
46  	/**
47  	 * Remove a constraint from the solver.
48  	 * 
49  	 * @param upl
50  	 * @since 2.1
51  	 */
52  	void remove(UnitPropagationListener upl);
53  
54  	/**
55  	 * Simplifies a constraint, by removing top level falsified literals for
56  	 * instance.
57  	 * 
58  	 * @return true iff the constraint is satisfied.
59  	 */
60  	boolean simplify();
61  
62  	/**
63  	 * Compute the reason for a given assignment.
64  	 * 
65  	 * If the constraint is a clause, it is supposed to be either a unit clause
66  	 * or a falsified one.
67  	 * 
68  	 * @param p
69  	 *            a satisfied literal (or Lit.UNDEFINED)
70  	 * @param outReason
71  	 *            the list of falsified literals whose negation is the reason of
72  	 *            the assignment of p to true.
73  	 */
74  	void calcReason(int p, IVecInt outReason);
75  
76  	/**
77  	 * Increase the constraint activity.
78  	 * 
79  	 * @param claInc
80  	 *            the value to increase the activity with
81  	 */
82  	void incActivity(double claInc);
83  
84  	/**
85  	 * 
86  	 * @param claInc
87  	 * @since 2.1
88  	 * 
89  	 */
90  	@Deprecated
91  	void forwardActivity(double claInc);
92  
93  	/**
94  	 * Indicate wether a constraint is responsible from an assignment.
95  	 * 
96  	 * @return true if a constraint is a "reason" for an assignment.
97  	 */
98  	boolean locked();
99  
100 	/**
101 	 * Mark a constraint as learnt.
102 	 */
103 
104 	void setLearnt();
105 
106 	/**
107 	 * Register the constraint to the solver.
108 	 */
109 	void register();
110 
111 	/**
112 	 * Rescale the clause activity by a value.
113 	 * 
114 	 * @param d
115 	 *            the value to rescale the clause activity with.
116 	 */
117 	void rescaleBy(double d);
118 
119 	/**
120 	 * Method called when the constraint is to be asserted. It means that the
121 	 * constraint was learnt during the search and it should now propagate some
122 	 * truth values. In the clausal case, only one literal should be propagated.
123 	 * In other cases, it might be different.
124 	 * 
125 	 * @param s
126 	 *            a UnitPropagationListener to use for unit propagation.
127 	 */
128 	void assertConstraint(UnitPropagationListener s);
129 }