Skip navigation
The Australian National University

Student research opportunities

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

Project Code: CECS_1099

This project is available at the following levels:
PhD
Please note that this project is only for higher degree (postgraduate) applicants.

Keywords:

logic, reasoning, satisfiability, automated reasoning, optimization, EPR

Supervisor:

Professor John Slaney

Outline:

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 of this project

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/Prerequisites

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/aistats14-1.pdf


Contact:



Updated:  10 August 2015 / Responsible Officer:  JavaScript must be enabled to display this email address. / Page Contact:  JavaScript must be enabled to display this email address. / Powered by: Snorkel 1.4