As good as it gets: maximal satisfiability for lifted EP theories

Research areas

Temporary Supervisor

Professor John Slaney

Description

EP (Effectively Propositional) problems are those expressed in first order logic which, when clausified, contain no function symbols other than constants. This fragment of logic is sometimes called "disjunctive datalog". Reasoning systems usually have great difficulty with problems in this class, because SAT solvers require them to be grounded, which may result in billions of clauses, while first order reasoners are unable to exploit the finiteness of the Herbrand universe. In this project, we aim to develop one or more solvers based on local search, specifically to find near-solutions to EPR problems which are globally unsatisfiable. Techniques for such MAX-SAT reasoning lifted to the first order level do exist, but they are too slow for the use we want to make of them in theorem proving. Fresh ideas are needed!

Goals

Advance the state of the art in local search for lifted (first order) maximum satisfiability problems over finite domains. In particular, produce a tool which can be used to guide a first-order theorem prover by providing semantic information about sets of clauses in the EP fragment of logic.

Requirements

Background in logic and computer science, preferably with some knowledge of automated reasoning. Programming is required, though the programming language(s) can be a matter of choice.

Background Literature

1. Slaney, J, Binas, A & Price, D 2004: 'Guiding a theorem prover with soft constraints', European Conference on Artificial Intelligence, pp. 221-225. 2. Sarkhel, S, Sigla, P & Gogate, V, 2014: 'Lifted MAP Inference for Markov Logic Networks', International Conference on Artificial Intelligence and Statistics. Paper online: http://www.hlt.utdallas.edu/~vgogate/papers/aistat...

Updated:  1 June 2019/Responsible Officer:  Dean, CECS/Page Contact:  CECS Marketing