pbsugar.encoder
Class PBEncoder
java.lang.Object
pbsugar.encoder.Encoder
pbsugar.encoder.PBEncoder
public class PBEncoder
- extends Encoder
Methods inherited from class pbsugar.encoder.Encoder |
close, code, decode, neg, newAuxVar, newVar, open, toString, toString, writeClause, writeClause, writeComment, writeComment |
TRUE_CNF
public static List<Clause> TRUE_CNF
FALSE_CNF
public static List<Clause> FALSE_CNF
countCM
public static int countCM
DECOMPOSE_PB
public static int DECOMPOSE_PB
countDecompose
public static int countDecompose
BASE
public static BigInteger BASE
ENCODE_CLAUSE_PART
public static boolean ENCODE_CLAUSE_PART
ENCODE_AS_CNF_LITERALS_SIZE
public static int ENCODE_AS_CNF_LITERALS_SIZE
SUM_CARRIES
public static boolean SUM_CARRIES
USE_CM_CACHE
public static boolean USE_CM_CACHE
CM_CACHE_SIZE
public static int CM_CACHE_SIZE
countCMreused
public static int countCMreused
SHARABLE_CM_LENGTH
public static int SHARABLE_CM_LENGTH
SHARABLE_CM_CACHE_SIZE
public static int SHARABLE_CM_CACHE_SIZE
countCMshared
public static int countCMshared
USE_SPARSE_CM
public static boolean USE_SPARSE_CM
PBEncoder
public PBEncoder(String satFileName)
pbLiteral
public int pbLiteral(PBLiteral lit)
singletonCNF
public List<Clause> singletonCNF(Clause clause)
or
public List<Clause> or(List<Clause> cs,
Clause c)
and
public List<Clause> and(List<Clause> cs,
Clause c)
or
public List<Clause> or(List<Clause> cs1,
List<Clause> cs2)
and
public List<Clause> and(List<Clause> cs1,
List<Clause> cs2)
encodeAsCNF
public List<Clause> encodeAsCNF(PBConstraint pb)
encodeClausePart
public PBConstraint encodeClausePart(PBConstraint pb,
List<Integer> literals,
List<Clause> clauses)
throws IOException
- Throws:
IOException
encodePB
public List<Clause> encodePB(PBConstraint pb)
throws IOException
- Throws:
IOException
encode
public void encode(PBConstraint pb)
throws IOException
- Throws:
IOException
PBSugar: SAT-based Pseudo Boolean Constraint Solver