PBSugar version 1.1.1 Core API Specification

pbsugar.encoder
Class PBEncoder

java.lang.Object
  extended by pbsugar.encoder.Encoder
      extended by pbsugar.encoder.PBEncoder

public class PBEncoder
extends Encoder


Field Summary
static BigInteger BASE
           
static int CM_CACHE_SIZE
           
static int countCM
           
static int countCMreused
           
static int countCMshared
           
static int countDecompose
           
static int DECOMPOSE_PB
           
static int ENCODE_AS_CNF_LITERALS_SIZE
           
static boolean ENCODE_CLAUSE_PART
           
static List<Clause> FALSE_CNF
           
static int SHARABLE_CM_CACHE_SIZE
           
static int SHARABLE_CM_LENGTH
           
static boolean SUM_CARRIES
           
static List<Clause> TRUE_CNF
           
static boolean USE_CM_CACHE
           
static boolean USE_SPARSE_CM
           
 
Fields inherited from class pbsugar.encoder.Encoder
debug, FALSE, sat, TRUE, UNDEF
 
Constructor Summary
PBEncoder(String satFileName)
           
 
Method Summary
 List<Clause> and(List<Clause> cs, Clause c)
           
 List<Clause> and(List<Clause> cs1, List<Clause> cs2)
           
 void encode(PBConstraint pb)
           
 List<Clause> encodeAsCNF(PBConstraint pb)
           
 PBConstraint encodeClausePart(PBConstraint pb, List<Integer> literals, List<Clause> clauses)
           
 List<Clause> encodePB(PBConstraint pb)
           
 List<Clause> or(List<Clause> cs, Clause c)
           
 List<Clause> or(List<Clause> cs1, List<Clause> cs2)
           
 int pbLiteral(PBLiteral lit)
           
 List<Clause> singletonCNF(Clause clause)
           
 
Methods inherited from class pbsugar.encoder.Encoder
close, code, decode, neg, newAuxVar, newVar, open, toString, toString, writeClause, writeClause, writeComment, writeComment
 
Methods inherited from class java.lang.Object
equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

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
Constructor Detail

PBEncoder

public PBEncoder(String satFileName)
Method Detail

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 version 1.1.1 Core API Specification

PBSugar: SAT-based Pseudo Boolean Constraint Solver