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

void	and(int y, int x1, int x2) Translate y <=> x1 /\ x2
void	and(int y, IVecInt literals) Translate y <=> x1 /\ x2 /\ ... /\ xn into clauses.
void	gateFalse(int y) translate y <=> FALSE into a clause.
void	gateTrue(int y) translate y <=> TRUE into a clause.
void	iff(int y, IVecInt literals) translate y <=> (x1 <=> x2 <=> ... <=> xn) into clauses.
void	ite(int y, int x1, int x2, int x3) translate y <=> if x1 then x2 else x3 into clauses.
void	not(int y, int x) Translate y <=> not x into clauses.
void	or(int y, IVecInt literals) translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.
void	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, addClause, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, model, model, nConstraints, newVar, newVar, nVars, printInfos, printStat, printStat, removeConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, 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 void 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.

gateTrue

public void gateTrue(int y)
              throws ContradictionException

translate y <=> TRUE into a clause.

Parameters:

y - a variable to verify

Throws:

ContradictionException

ite

public void 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

and

public void and(int y,
                IVecInt literals)
         throws ContradictionException

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

Parameters:

y -

literals - the x1 ... xn literals.

Throws:

ContradictionException

and

public void and(int y,
                int x1,
                int x2)
         throws ContradictionException

Translate y <=> x1 /\ x2

Parameters:

y -

x1 -

x2 -

Throws:

ContradictionException

or

public void or(int y,
               IVecInt literals)
        throws ContradictionException

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

Parameters:

y -

literals -

Throws:

ContradictionException

not

public void not(int y,
                int x)
         throws ContradictionException

Translate y <=> not x into clauses.

Parameters:

y -

x -

Throws:

ContradictionException

xor

public void xor(int y,
                IVecInt literals)
         throws ContradictionException

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

Parameters:

y -

literals -

Throws:

ContradictionException

iff

public void iff(int y,
                IVecInt literals)
         throws ContradictionException

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

Parameters:

y -

literals -

Throws:

ContradictionException