org.sat4j.minisat.constraints.cnf
Class Clauses

java.lang.Object
  extended by org.sat4j.minisat.constraints.cnf.Clauses

public abstract class Clauses
extends Object

Since:
2.1
Author:
daniel

Constructor Summary
Clauses()
           
 
Method Summary
static IVecInt sanityCheck(IVecInt ps, ILits voc, UnitPropagationListener s)
          Perform some sanity check before constructing a clause a) if a literal is assigned true, return null (the clause is satisfied) b) if a literal is assigned false, remove it c) if a clause contains a literal and its opposite (tautology) return null d) remove duplicate literals e) if the clause is empty, return null f) if the clause if unit, transmit it to the object responsible for unit propagation
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

Clauses

public Clauses()
Method Detail

sanityCheck

public static IVecInt sanityCheck(IVecInt ps,
                                  ILits voc,
                                  UnitPropagationListener s)
                           throws ContradictionException
Perform some sanity check before constructing a clause a) if a literal is assigned true, return null (the clause is satisfied) b) if a literal is assigned false, remove it c) if a clause contains a literal and its opposite (tautology) return null d) remove duplicate literals e) if the clause is empty, return null f) if the clause if unit, transmit it to the object responsible for unit propagation

Parameters:
ps - the list of literals
voc - the vocabulary used
s - the object responsible for unit propagation
Returns:
null if the clause should be ignored, the (possibly modified) list of literals otherwise
Throws:
ContradictionException - if discovered by unit propagation


Copyright © 2010 Centre de Recherche en Informatique de Lens (CRIL). All Rights Reserved.