tuffy.infer.ds
Class GAtom

java.lang.Object
  tuffy.infer.ds.GAtom

public class GAtom
extends java.lang.Object

A ground atom.

Field Summary

boolean	cut Whether this atom is referred to by multiple partitions
boolean	fixed Whether the truth value of this GAtom is fixed.
int	id ID of this GAtom.
boolean	lowlowTruth
boolean	lowTruth Recorded truth value for low-cost.
int	pid ID of the partition containing this atom
float	prob
java.lang.String	rep String representation of this GAtom.
private double	rescue Two cost of changing the truth value of this GAtom.
int	tallyTrue Tallies used in MCSAT.
boolean	truth The truth value of this GAtom.
private double	violate Two cost of changing the truth value of this GAtom.
int	wannabe The ideal truth value of this GAtom.

Constructor Summary

GAtom(int nid)
Constructor for GAtom.

Method Summary

void	assignSatPotential(GClause f) Flipping this node will make f unsat->sat.
void	assignUnsatPotential(GClause f) Flipping this node will make f sat->unsat.
boolean	critical() Whether wannabe == 3.
boolean	criticalForHardClauses() Whether changing the truth value of this GAtom will violate several hard clauses.
double	delta()
double	delta(KeyBlock keyBlock)
void	flip() Flip the truth value of this GAtom.
java.util.ArrayList<GAtom>	flip(KeyBlock keyBlock)
void	forceFlip()
void	invertDelta() Exchange the value of rescue and violate.
void	markCritical() Set wannabe = 3.
void	markWannaBeFalse() Set wannabe = 1.
void	markWannaBeTrue() Set wannabe = 2.
void	resetDelta() Reset rescue and violate to zero.
void	revokeSatPotential(GClause f) Flipping this node no longer makes f unsat->sat.
void	revokeUnsatPotential(GClause f) Flipping this node no longer makes f sat->unsat.
boolean	wannaBeFalse() Whether wannabe == 1; (false)
boolean	wannaBeTrue() Whether wannabe == 2; (true)

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

id

public int id

ID of this GAtom.

pid

public int pid

ID of the partition containing this atom

cut

public boolean cut

Whether this atom is referred to by multiple partitions

truth

public boolean truth

The truth value of this GAtom.

wannabe

public int wannabe

The ideal truth value of this GAtom. 1 = false; 2 = true; 3 = both.

lowTruth

public boolean lowTruth

Recorded truth value for low-cost.

lowlowTruth

public boolean lowlowTruth

fixed

public boolean fixed

Whether the truth value of this GAtom is fixed.

tallyTrue

public int tallyTrue

Tallies used in MCSAT.

prob

public float prob

violate

private double violate

Two cost of changing the truth value of this GAtom. Violate is the cost that will increases after flipping. Rescue is the cost that will decreases after flipping.

rescue

private double rescue

Two cost of changing the truth value of this GAtom. Violate is the cost that will increases after flipping. Rescue is the cost that will decreases after flipping.

rep

public java.lang.String rep

String representation of this GAtom.

Constructor Detail

GAtom

public GAtom(int nid)

Constructor for GAtom.

Parameters:

nid - ID of this GAtom.

Method Detail

critical

public boolean critical()

Whether wannabe == 3. (both)

wannaBeFalse

public boolean wannaBeFalse()

Whether wannabe == 1; (false)

wannaBeTrue

public boolean wannaBeTrue()

Whether wannabe == 2; (true)

markCritical

public void markCritical()

Set wannabe = 3. (both)

markWannaBeFalse

public void markWannaBeFalse()

Set wannabe = 1. (false)

markWannaBeTrue

public void markWannaBeTrue()

Set wannabe = 2. (true)

flip

public void flip()

Flip the truth value of this GAtom.

forceFlip

public void forceFlip()

flip

public java.util.ArrayList<GAtom> flip(KeyBlock keyBlock)

resetDelta

public void resetDelta()

Reset rescue and violate to zero.

invertDelta

public void invertDelta()

Exchange the value of rescue and violate. When the truth value of this GAtom is flipped, this function is called.

criticalForHardClauses

public boolean criticalForHardClauses()

Whether changing the truth value of this GAtom will violate several hard clauses.

delta

public double delta()

Returns:

Delta to the total cost if this node is flipped.

delta

public double delta(KeyBlock keyBlock)

Returns:

Delta to the total cost if this node is flipped.

assignSatPotential

public void assignSatPotential(GClause f)

Flipping this node will make f unsat->sat.

Parameters:

f - GClause that currently not registered.

assignUnsatPotential

public void assignUnsatPotential(GClause f)

Flipping this node will make f sat->unsat.

Parameters:

f - GClause that currently not registered.

revokeSatPotential

public void revokeSatPotential(GClause f)

Flipping this node no longer makes f unsat->sat.

Parameters:

f - GClause that currently registered as unsat->sat.

revokeUnsatPotential

public void revokeUnsatPotential(GClause f)

Flipping this node no longer makes f sat->unsat.

Parameters:

f - GClause that currently registered as sat->unsat.