org.sat4j.minisat.constraints.cnf
Class OriginalBinaryClause

java.lang.Object
  org.sat4j.minisat.constraints.cnf.BinaryClause
      org.sat4j.minisat.constraints.cnf.OriginalBinaryClause

All Implemented Interfaces:

java.io.Serializable, Constr, Propagatable, IConstr

public class OriginalBinaryClause
extends BinaryClause

SAT4J: a SATisfiability library for Java Copyright (C) 2004-2008 Daniel Le Berre All rights reserved. This program and the accompanying materials are made available under the terms of the Eclipse Public License v1.0 which accompanies this distribution, and is available at http://www.eclipse.org/legal/epl-v10.html Alternatively, the contents of this file may be used under the terms of either the GNU Lesser General Public License Version 2.1 or later (the "LGPL"), in which case the provisions of the LGPL are applicable instead of those above. If you wish to allow use of your version of this file only under the terms of the LGPL, and not to allow others to use your version of this file under the terms of the EPL, indicate your decision by deleting the provisions above and replace them with the notice and other provisions required by the LGPL. If you do not delete the provisions above, a recipient may use your version of this file under the terms of the EPL or the LGPL. Based on the original MiniSat specification from: An extensible SAT solver. Niklas Een and Niklas Sorensson. Proceedings of the Sixth International Conference on Theory and Applications of Satisfiability Testing, LNCS 2919, pp 502-518, 2003. See www.minisat.se for the original solver in C++.

See Also:

Serialized Form

Constructor Summary

OriginalBinaryClause(IVecInt ps, ILits voc)

Method Summary

static OriginalBinaryClause	brandNewClause(UnitPropagationListener s, ILits voc, IVecInt literals) Creates a brand new clause, presumably from external data.
boolean	learnt()
void	setLearnt() Mark a constraint as learnt.

Methods inherited from class org.sat4j.minisat.constraints.cnf.BinaryClause

assertConstraint, calcReason, equals, get, getActivity, getLits, getVocabulary, hashCode, incActivity, locked, propagate, register, remove, rescaleBy, simplify, size, toString

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Constructor Detail

OriginalBinaryClause

public OriginalBinaryClause(IVecInt ps,
                            ILits voc)

Method Detail

setLearnt

public void setLearnt()

Description copied from interface: Constr

Mark a constraint as learnt.

learnt

public boolean learnt()

Returns:

true iff the clause was learnt during the search

brandNewClause

public static OriginalBinaryClause brandNewClause(UnitPropagationListener s,
                                                  ILits voc,
                                                  IVecInt literals)

Creates a brand new clause, presumably from external data.

Parameters:

s - the object responsible for unit propagation

voc - the vocabulary

literals - the literals to store in the clause

Returns:

the created clause or null if the clause should be ignored (tautology for example)