org.sat4j.minisat.constraints.cnf
Class Clauses

java.lang.Object
  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