org.sat4j.tools
Class GateTranslator

java.lang.Object
  org.sat4j.tools.SolverDecorator<ISolver>
      org.sat4j.tools.GateTranslator

All Implemented Interfaces:

java.io.Serializable, IProblem, ISolver

public class GateTranslator
extends SolverDecorator<ISolver>

Utility class to easily feed a SAT solver using logical gates.

Author:

leberre

See Also:

Serialized Form

Constructor Summary

GateTranslator(ISolver solver)

Method Summary

IConstr[]	and(int y, int x1, int x2) Translate y <=> x1 /\ x2
IConstr[]	and(int y, IVecInt literals) Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.
IConstr	gateFalse(int y) translate y <=> FALSE into a clause.
IConstr	gateTrue(int y) translate y <=> TRUE into a clause.
IConstr[]	iff(int y, IVecInt literals) translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.
IConstr[]	ite(int y, int x1, int x2, int x3) translate y <=> if x1 then x2 else x3 into clauses.
IConstr[]	not(int y, int x) Translate y <=> not x into clauses.
IConstr[]	or(int y, IVecInt literals) translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.
IConstr[]	xor(int y, IVecInt literals) translate y <=> x1 xor x2 xor ... xor xn into clauses.

Methods inherited from class org.sat4j.tools.SolverDecorator

addAllClauses, addAtLeast, addAtMost, addBlockingClause, addClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, newVar, newVar, nextFreeVarId, nVars, printInfos, printStat, printStat, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, toString

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

GateTranslator

public GateTranslator(ISolver solver)

Method Detail

gateFalse

public IConstr gateFalse(int y)
                  throws ContradictionException

translate y <=> FALSE into a clause.

Parameters:

y - a variable to falsify

Throws:

ContradictionException - iff a trivial inconsistency is found.

Since:

2.1

gateTrue

public IConstr gateTrue(int y)
                 throws ContradictionException

translate y <=> TRUE into a clause.

Parameters:

y - a variable to verify

Throws:

ContradictionException

Since:

2.1

ite

public IConstr[] ite(int y,
                     int x1,
                     int x2,
                     int x3)
              throws ContradictionException

translate y <=> if x1 then x2 else x3 into clauses.

Parameters:

y -

x1 - the selector variable

x2 -

x3 -

Throws:

ContradictionException

Since:

2.1

and

public IConstr[] and(int y,
                     IVecInt literals)
              throws ContradictionException

Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.

Parameters:

y -

literals - the x1 ... xn literals.

Throws:

ContradictionException

Since:

2.1

and

public IConstr[] and(int y,
                     int x1,
                     int x2)
              throws ContradictionException

Translate y <=> x1 /\ x2

Parameters:

y -

x1 -

x2 -

Throws:

ContradictionException

Since:

2.1

or

public IConstr[] or(int y,
                    IVecInt literals)
             throws ContradictionException

translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.

Parameters:

y -

literals -

Throws:

ContradictionException

Since:

2.1

not

public IConstr[] not(int y,
                     int x)
              throws ContradictionException

Translate y <=> not x into clauses.

Parameters:

y -

x -

Throws:

ContradictionException

Since:

2.1

xor

public IConstr[] xor(int y,
                     IVecInt literals)
              throws ContradictionException

translate y <=> x1 xor x2 xor ... xor xn into clauses.

Parameters:

y -

literals -

Throws:

ContradictionException

Since:

2.1

iff

public IConstr[] iff(int y,
                     IVecInt literals)
              throws ContradictionException

translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.

Parameters:

y -

literals -

Throws:

ContradictionException

Since:

2.1