StatSat Bibliography

An artificial neural network tester for the satisfiability problem of propositional calculus is presented. Satisfiability is treated as a constraint satisfaction optimization problem and, contrary to most of the existing satisfiability testers, the expressions are converted into disjunctive normal form before testing. The artificial neural network is based on the principles of harmony theory. Its basic characteristics are the simulated annealing procedure and the harmony function; the latter constitutes a measure of the satisfiability of the expression under the current truth assignment to its variables. The tester is such that: (a) the satisfiability of any expression is determined; (b) a truth assignment to the variables of the expression is output which renders true the greatest possible number of clauses; (c) all the truth assignments which render true the maximum number of clauses can be produced. (c) 2001 John Wiley & Sons, Inc.

Abstract. We propose a simple approach to combining rst-order logic and probabilistic graphical models in a single representation. A Markov logic network (MLN) is a rst-order knowledge base with a weight attached to each formula (or clause). Together with a set of constants representing objects in the domain, it speci es a ground Markov network containing one feature for each possible grounding of a rst-order formula in the KB, with the corresponding weight. Inference in MLNs is performed by MCMC over the minimal subset of the ground network required for answering the query. Weights are ef ciently learned from relational databases by iteratively optimizing a pseudo-likelihood measure. Optionally, additional clauses are learned using inductive logic programming techniques. Experiments with a real-world database and knowledge base in a university domain illustrate the promise of this approach.