MC-SAT Algorithm
A MC-SAT Algorithm is an Inference Algorithm that is based on Markov logic combining MCMC and satisfiability methods.
- Context:
- It is a Slice Sampling Algorithm.
- Example(s):
- the algorithm described in Poon & Domingos (2006).
- …
- Counter-Example(s):
- See: Markov Network, First-Order Logic System, Entity Reference Grounding Task.
References
2007
- (Poon & Domingos, 2007) ⇒ Hoifung Poon, and Pedro Domingos. (2007). “Joint inference in information extraction.” In: Proceedings of the Twenty-Second National Conference on Artificial Intelligence (AAAI 2007).
- QUOTE: Markov logic makes it possible to compactly specify probability distributions over complex relational domains. We used the learning and inference algorithms provided in the open-source Alchemy package (Kok et al. 2006). In particular, we performed inference using the MC-SAT algorithm (Poon & Domingos 2006), and discriminative weight learning using the voted perceptron algorithm (Singla & Domingos 2005).
MC-SAT is a “slice sampling” Markov chain Monte Carlo algorithm. It uses a combination of satisfiability testing and simulated annealing to sample from the slice. The advantage of using a satisfiability solver (WalkSAT) is that it efficiently finds isolated modes in the distribution, and as a result the Markov chain mixes very rapidly. The slice sampling scheme ensures that detailed balance is (approximately) preserved. MC-SAT is orders of magnitude faster than previous MCMC algorithms like Gibbs sampling and simulated tempering, and makes efficient joint inference possible on a scale that was previously out of reach. In this paper, we use it to perform inference over hundreds of thousands of variables in tens of minutes.
- QUOTE: Markov logic makes it possible to compactly specify probability distributions over complex relational domains. We used the learning and inference algorithms provided in the open-source Alchemy package (Kok et al. 2006). In particular, we performed inference using the MC-SAT algorithm (Poon & Domingos 2006), and discriminative weight learning using the voted perceptron algorithm (Singla & Domingos 2005).
2006
- (Poon & Domingos, 2006) ⇒ Hoifung Poon, and Pedro Domingos. (2006). “ Sound and Efficient Inference with Probabilistic and Deterministic Dependencies.” In: Proceedings of the 21st national conference on Artificial intelligence. AAAI 2006. ISBN:978-1-57735-281-5
- QUOTE: MC-SAT applies slice sampling to Markov logic, using SampleSAT to sample a new state given the auxiliary variables. In the Markov network obtained by applying an MLN to a set of constants, each ground clause [math]\displaystyle{ c_k }[/math] [math]\displaystyle{ c_k }[/math] corresponds to the potential function [math]\displaystyle{ \phi_k(x) = exp(w_k\;f_k(x)) }[/math], which has value [math]\displaystyle{ e^{w_k} }[/math] if [math]\displaystyle{ c_k }[/math] is satisfied, and 1 otherwise. We introduce an auxiliary variable [math]\displaystyle{ u_k }[/math] for each [math]\displaystyle{ c_k }[/math]. Assume for the moment that all weights are non-negative. On the ith iteration of MC-SAT, if [math]\displaystyle{ c_k }[/math] is not satisfied by the current state [math]\displaystyle{ x^{(i)} }[/math], [math]\displaystyle{ u_k }[/math] is drawn uniformly from [math]\displaystyle{ [0, 1] }[/math]; therefore [math]\displaystyle{ u_k \leq 1 }[/math] and [math]\displaystyle{ u_k \leq e^{w_i} }[/math] , and there is no requirement that it be satisfied in the next state. If [math]\displaystyle{ c_k }[/math] is satisfied, [math]\displaystyle{ u_k }[/math] is drawn uniformly from [math]\displaystyle{ [0, e^{w_i} ] }[/math], and with probability [math]\displaystyle{ 1−e^{−w_i} }[/math] it will be greater than 1, in which case the next state must satisfy [math]\displaystyle{ c_k }[/math]. Thus, sampling all the auxiliary variables determines a random subset [math]\displaystyle{ M }[/math] of the currently satisfied clauses that must also be satisfied in the next state. We then take as the next state a uniform sample from the set of states [math]\displaystyle{ SAT (M) }[/math] that satisfy [math]\displaystyle{ M }[/math]. (Notice that [math]\displaystyle{ SAT (M) }[/math] is never empty, because it always contains at least the current state.) The initial state is found by applying a satisfiability solver to the set of all hard clauses in the network (i.e., all clauses with infinite weight). If this set is unsatisfiable, the output of MC-SAT is undefined.
Algorithm 1 gives pseudo-code for MC-SAT. [math]\displaystyle{ \mathcal{U}_S }[/math] is the uniform distribution over set [math]\displaystyle{ S }[/math]. At each step, all hard clauses are selected with probability 1, and thus all sampled states satisfy them. For brevity, the code ignores the case of negative weights. These are handled by noting that a clause with weight [math]\displaystyle{ w \lt 0 }[/math] is equivalent to its negation with weight [math]\displaystyle{ −w }[/math], and a clause’s negation is the conjunction of the negations of all of its literals. Thus, instead of checking whether the clause is satisfied; if it is, with probability [math]\displaystyle{ 1 − e^w }[/math] we select all of its negated literals, and with probability [math]\displaystyle{ e^w }[/math] we select none.
- QUOTE: MC-SAT applies slice sampling to Markov logic, using SampleSAT to sample a new state given the auxiliary variables. In the Markov network obtained by applying an MLN to a set of constants, each ground clause [math]\displaystyle{ c_k }[/math] [math]\displaystyle{ c_k }[/math] corresponds to the potential function [math]\displaystyle{ \phi_k(x) = exp(w_k\;f_k(x)) }[/math], which has value [math]\displaystyle{ e^{w_k} }[/math] if [math]\displaystyle{ c_k }[/math] is satisfied, and 1 otherwise. We introduce an auxiliary variable [math]\displaystyle{ u_k }[/math] for each [math]\displaystyle{ c_k }[/math]. Assume for the moment that all weights are non-negative. On the ith iteration of MC-SAT, if [math]\displaystyle{ c_k }[/math] is not satisfied by the current state [math]\displaystyle{ x^{(i)} }[/math], [math]\displaystyle{ u_k }[/math] is drawn uniformly from [math]\displaystyle{ [0, 1] }[/math]; therefore [math]\displaystyle{ u_k \leq 1 }[/math] and [math]\displaystyle{ u_k \leq e^{w_i} }[/math] , and there is no requirement that it be satisfied in the next state. If [math]\displaystyle{ c_k }[/math] is satisfied, [math]\displaystyle{ u_k }[/math] is drawn uniformly from [math]\displaystyle{ [0, e^{w_i} ] }[/math], and with probability [math]\displaystyle{ 1−e^{−w_i} }[/math] it will be greater than 1, in which case the next state must satisfy [math]\displaystyle{ c_k }[/math]. Thus, sampling all the auxiliary variables determines a random subset [math]\displaystyle{ M }[/math] of the currently satisfied clauses that must also be satisfied in the next state. We then take as the next state a uniform sample from the set of states [math]\displaystyle{ SAT (M) }[/math] that satisfy [math]\displaystyle{ M }[/math]. (Notice that [math]\displaystyle{ SAT (M) }[/math] is never empty, because it always contains at least the current state.) The initial state is found by applying a satisfiability solver to the set of all hard clauses in the network (i.e., all clauses with infinite weight). If this set is unsatisfiable, the output of MC-SAT is undefined.
