infer
Class MCSAT

java.lang.Object
  extended by infer.MRF
      extended by infer.MCSAT

public class MCSAT
extends MRF

The MC-SAT algorithm for marginal inference. http://www.cs.washington.edu/homes/pedrod/papers/aaai08c.pdf


Field Summary
 java.util.HashMap<java.lang.String,java.lang.Long> clauseNiNjViolationTallies
          This map records the tallies for calculating E(v_i*v_j).
 java.util.HashMap<java.lang.String,java.lang.Long> clauseSatTallies
          This array records total number of satisfaction for a clause.
 java.util.HashMap<java.lang.String,java.lang.Long> clauseSquareVioTallies
          This array records total number of square violation for a clause.
 java.util.HashMap<java.lang.String,java.lang.Long> clauseVioTallies
          This array records total number of violation for a clause.
 java.util.HashMap<java.lang.String,java.lang.Double> expectationOfNiNjViolation
          This map records the expectation of E(v_i*v_j).
 java.util.HashMap<java.lang.String,java.lang.Double> expectationOfSatisfication
          This array records the expection of #satisfaction for each clause.
 java.util.HashMap<java.lang.String,java.lang.Double> expectationOfSquareViolation
          This map records the expectation of square #violation for each clause.
 java.util.HashMap<java.lang.String,java.lang.Double> expectationOfViolation
          This map records the expectation of #violation for each clause.
 int nClauseVioTallies
          Number of iterations of tallies.
 
Fields inherited from class infer.MRF
adj, atoms, clauses, dirtyAtoms, fout, inferOps, lowCost, sampleSatMode, totalAlive, totalCost, unsat
 
Constructor Summary
MCSAT(Grounding grounding)
          Constructor of MCSAT.
 
Method Summary
 void calcExpViolation()
          Calculating the different expectations by filling the HashMaps related to expectations in this class.
 void dumpAtomProb(int numSamples, java.lang.String fout)
          Dump result of MCSAT inference to output file.
 void flushNewWeight2DB(java.util.HashMap<java.lang.String,java.lang.Double> currentWeight)
          Change the weight of GClause based on updated weight of Clause.
 void mcsat(int numSamples, int numFlips)
          Execute the MC-SAT algorithm.
protected  int retainOnlyHardClauses()
          Kill soft clauses.
 boolean sampleSAT(int nSteps)
          SampleSAT (with WalkSAT inside), used to uniformly sample a zero-cost world.
protected  void updateAtomTruthTallies()
          For each atom, increment its truth tally by one if it's currently true.
 void updateClauseVoiTallies()
          Update the number of violations of a clause.
 
Methods inherited from class infer.MRF
addAtom, auditClauseViolations, buildIndices, calcCosts, discard, enableAllClauses, fixAtom, flushLowTruth, inferSweepSAT, inferWalkSAT, initMRF, invalidateLowCost, isAlwaysTrue, isTrueLit, loadMRF, ownsAtom, recalcCost, restoreLowTruth, retainSomeGoodClauses, saveLowTruth, testChance, unfixAllAtoms
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

clauseNiNjViolationTallies

public java.util.HashMap<java.lang.String,java.lang.Long> clauseNiNjViolationTallies
This map records the tallies for calculating E(v_i*v_j).


clauseSatTallies

public java.util.HashMap<java.lang.String,java.lang.Long> clauseSatTallies
This array records total number of satisfaction for a clause.


clauseSquareVioTallies

public java.util.HashMap<java.lang.String,java.lang.Long> clauseSquareVioTallies
This array records total number of square violation for a clause. Dividing this number by nClauseVioTallies will give the estimated expectation of #violation.


clauseVioTallies

public java.util.HashMap<java.lang.String,java.lang.Long> clauseVioTallies
This array records total number of violation for a clause. Dividing this number by nClauseVioTallies will give the estimated expectation of #violation.


expectationOfNiNjViolation

public java.util.HashMap<java.lang.String,java.lang.Double> expectationOfNiNjViolation
This map records the expectation of E(v_i*v_j). This is filled by calcExpViolation().


expectationOfSatisfication

public java.util.HashMap<java.lang.String,java.lang.Double> expectationOfSatisfication
This array records the expection of #satisfaction for each clause. This is filled by calcExpViolation().


expectationOfSquareViolation

public java.util.HashMap<java.lang.String,java.lang.Double> expectationOfSquareViolation
This map records the expectation of square #violation for each clause. This is filled by calcExpViolation().


expectationOfViolation

public java.util.HashMap<java.lang.String,java.lang.Double> expectationOfViolation
This map records the expectation of #violation for each clause. This is filled by calcExpViolation().


nClauseVioTallies

public int nClauseVioTallies
Number of iterations of tallies.

Constructor Detail

MCSAT

public MCSAT(Grounding grounding)
Constructor of MCSAT.

Parameters:
grounding - Grounding worker based on which this MCSAT instance forms the MRF.
Method Detail

calcExpViolation

public void calcExpViolation()
Calculating the different expectations by filling the HashMaps related to expectations in this class.


dumpAtomProb

public void dumpAtomProb(int numSamples,
                         java.lang.String fout)
Dump result of MCSAT inference to output file.

Parameters:
numSamples - number of samples in this MCSAT inference. This is used to estimate the probability of an atom being true.
fout - Name of output file.

flushNewWeight2DB

public void flushNewWeight2DB(java.util.HashMap<java.lang.String,java.lang.Double> currentWeight)
Change the weight of GClause based on updated weight of Clause. This new weight will be aware by MCSAT. The cost of flipping atom and the unsat set for GClause will be calculated automatically by this function.

Parameters:
currentWeight - The weight of clauses to be flushed in this MCSAT instance.

mcsat

public void mcsat(int numSamples,
                  int numFlips)
Execute the MC-SAT algorithm.

Parameters:
numSamples - number of MC-SAT samples
numFlips - number of SampleSAT steps in each iteration

retainOnlyHardClauses

protected int retainOnlyHardClauses()
Kill soft clauses.

Returns:
the number of hard clauses

sampleSAT

public boolean sampleSAT(int nSteps)
SampleSAT (with WalkSAT inside), used to uniformly sample a zero-cost world. WalkSAT is used as a SAT solver to find the first (quasi-)zero-cost world. Simulated annealing (SA) is stochastically performed to wander around.

Parameters:
nSteps -

updateAtomTruthTallies

protected void updateAtomTruthTallies()
For each atom, increment its truth tally by one if it's currently true.


updateClauseVoiTallies

public void updateClauseVoiTallies()
Update the number of violations of a clause. For each GClause, their value can increase at most 1 for each MCSAT iteration. For Clause, their value can increase more, because there may be more than one GClauses associated with it.