org.sat4j.tools
Class GateTranslator

java.lang.Object
  extended by org.sat4j.tools.SolverDecorator<ISolver>
      extended by 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


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