org.sat4j.tools
Class GateTranslator

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

All Implemented Interfaces:

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	additionalFullAdderConstraints(int xcarry, int xsum, int a, int b, int c)
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.
void	fullAdderCarry(int x, int a, int b, int c)
void	fullAdderSum(int x, int a, int b, int c)
IConstr	gateFalse(int y) translate y <=> FALSE into a clause.
IConstr	gateTrue(int y) translate y <=> TRUE into a clause.
void	halfAdderCarry(int x, int a, int b)
void	halfAdderSum(int x, int a, int b)
IConstr[]	halfOr(int y, IVecInt literals) translate y <= x1 \/ x2 \/ ... \/ xn into clauses.
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.
void	optimisationFunction(IVecInt literals, IVec<BigInteger> coefs, IVecInt result) Translate an optimization function into constraints and provides the binary literals in results.
IConstr[]	or(int y, IVecInt literals) translate y <=> x1 \/ x2 \/ ... \/ xn into clauses.
void	xor(int x, int a, int b)
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, addExactly, clearDecorated, clearLearntClauses, decorated, expireTimeout, findModel, findModel, getLogPrefix, getSearchListener, getStat, getTimeout, getTimeoutMs, isDBSimplificationAllowed, isSatisfiable, isSatisfiable, isSatisfiable, isSatisfiable, isSolverKeptHot, isVerbose, model, model, modelWithInternalVariables, nConstraints, newVar, newVar, nextFreeVarId, nVars, primeImplicant, primeImplicant, printInfos, printStat, printStat, realNumberOfVariables, registerLiteral, removeConstr, removeSubsumedConstr, reset, setDBSimplificationAllowed, setExpectedNumberOfClauses, setKeepSolverHot, setLogPrefix, setSearchListener, setTimeout, setTimeoutMs, setTimeoutOnConflicts, setVerbose, toString, toString, unsatExplanation

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, 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

halfOr

public IConstr[] halfOr(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

xor

public void xor(int x,
                int a,
                int b)
         throws ContradictionException

Throws:

ContradictionException

Since:

2.2

fullAdderSum

public void fullAdderSum(int x,
                         int a,
                         int b,
                         int c)
                  throws ContradictionException

Throws:

ContradictionException

Since:

2.2

fullAdderCarry

public void fullAdderCarry(int x,
                           int a,
                           int b,
                           int c)
                    throws ContradictionException

Throws:

ContradictionException

Since:

2.2

additionalFullAdderConstraints

public void additionalFullAdderConstraints(int xcarry,
                                           int xsum,
                                           int a,
                                           int b,
                                           int c)
                                    throws ContradictionException

Throws:

ContradictionException

Since:

2.2

halfAdderSum

public void halfAdderSum(int x,
                         int a,
                         int b)
                  throws ContradictionException

Throws:

ContradictionException

Since:

2.2

halfAdderCarry

public void halfAdderCarry(int x,
                           int a,
                           int b)
                    throws ContradictionException

Throws:

ContradictionException

Since:

2.2

optimisationFunction

public void optimisationFunction(IVecInt literals,
                                 IVec<BigInteger> coefs,
                                 IVecInt result)
                          throws ContradictionException

Translate an optimization function into constraints and provides the binary literals in results. Works only when the value of the objective function is positive.

Throws:

ContradictionException

Since:

2.2