jp.ac.kobe_u.cs.sugar.encoder
Class Encoder
java.lang.Object
jp.ac.kobe_u.cs.sugar.encoder.Encoder
public class Encoder
- extends Object
Encoder encodes CSP into SAT.
- See Also:
CSP
satSolverName
public static String satSolverName
FALSE_CODE
public static final int FALSE_CODE
- See Also:
- Constant Field Values
TRUE_CODE
public static final int TRUE_CODE
- See Also:
- Constant Field Values
USE_NEWIO
public static boolean USE_NEWIO
SAT_BUFFER_SIZE
public static int SAT_BUFFER_SIZE
MAX_SAT_SIZE
public static long MAX_SAT_SIZE
Encoder
public Encoder(CSP csp)
negateCode
public static int negateCode(int code)
getSatClausesCount
public int getSatClausesCount()
getSatFileSize
public long getSatFileSize()
flush
public void flush()
throws IOException
- Throws:
IOException
write
public void write(String s)
throws IOException
- Throws:
IOException
writeComment
public void writeComment(String comment)
throws IOException
- Throws:
IOException
writeClause
public void writeClause(int[] clause)
throws IOException
- Throws:
IOException
writeClause
public void writeClause(List<Integer> clause0)
throws IOException
- Throws:
IOException
getHeader
public String getHeader(int numOfVariables,
int numOfClauses)
throws UnsupportedEncodingException
- Throws:
UnsupportedEncodingException
encode
public void encode(String satFileName,
boolean incremental)
throws SugarException,
IOException
- Throws:
SugarException
IOException
modifySat
public void modifySat(String satFileName,
int[][] clauses)
throws IOException
- Throws:
IOException
modifySat
public void modifySat(String satFileName,
int[] clause)
throws IOException
- Throws:
IOException
outputMap
public void outputMap(String mapFileName)
throws SugarException,
IOException
- Throws:
SugarException
IOException
decode
public boolean decode(String outFileName)
throws SugarException,
IOException
- Throws:
SugarException
IOException
summary
public String summary()
Sugar: A SAT-based Constraint Solver