Academic
Publications
New Techniques that Improve MACE-style Finite Model Finding

New Techniques that Improve MACE-style Finite Model Finding,Koen Claessen,Niklas Sorensson

New Techniques that Improve MACE-style Finite Model Finding   (Citations: 62)
BibTex | RIS | RefWorks Download
We describe a new method for finding finite models of unsorted first-order logic clause sets. The method is a MACE-style method, i.e. it "flattens" the first-order clauses, and for increasing model sizes, instanti- ates the resulting clauses into propositional clauses which are consecutively solved by a SAT-solver. We enhance the standard method by using 4 novel techniques: term definitions, which reduce the number of variables in flat- tened clauses, incremental SAT, which enables reuse of search information between consecutive model sizes, static symmetry reduction, which reduces the number of isomorphic models by adding extra constraints to the SAT problem, and sort inference, which allows the symmetry reduction to be ap- plied at a finer grain. All techniques have been implemented in a new model finder, called Paradox, with very promising results.
Published in 2003.
Cumulative Annual
    • ...Paradox [7] can be used for finding finite models of general first-order formulas...

    Ruzica Piskacet al. Deciding Effectively Propositional Logic Using DPLL and Substitution S...

    • ...Other methods for nite model computation essentially work by stepwise reduction to formulas in propositional logic and use a SAT solver on the result. [Sla94, McC94, ZZ95, CS03, Pel03b, e.g.]...

    Peter Baumgartneret al. Instance Based Methods - A Brief Overview

    • ...In translational approaches [7,8], the FMC problem is divided into multiple satisfiability problems in propositional logic...
    • ...iClingo solved the same number of problems as Paradox [8] in approximately half of its run time on average...
    • ...Any first-order clause can be transformed into an equisatisfiable flat clause via flattening [7,8,6], done by repeatedly applying the rewrite rule C[t] (C[X]∨(X � t)) ,w heret is a term offending flatness and X is a fresh variable...
    • ...To this end, we use the technique described in [8,15], fixing an order of the constants in the input by uniquely assigning ar ank in[1 ,n ] ,w heren is the total number of constants, to each of them...
    • ...For the special case of unary functions, such an extension [8] is implemented in Paradox; with FM-Darwin, it has not turned out to be more effective than symmetry breaking for only constants [15]...
    • ...The fact that the underlying first-order theory has many sorts, so that sort inference [8] of Paradox helps, shows that there is still potential to improve the translational approach via iASP...

    Martin Gebseret al. An Incremental Answer Set Programming Based System for Finite ModelCom...

    • ...The MACE-style model builder with the best performance today is perhaps the Paradox system [CS03]...
    • ...is implemented in our approach and many others (Paradox [CS03], Finder [Sla92], Mace [McC94], Mace4 [McC03] , SEM [Zha95] toname a few)...
    • ...Our reduction to clause sets encoding finite E-satisfiability is similar to, and indeed inspired by, the one in Paradox [CS03]...
    • ...This has the advantage of often being more space-efficient: i n Paradox, as the domain size d is increased, the number of ground instances of a clause grows exponentially in the number of variables in the clause [CS03]...

    Peter Baumgartneret al. Computing finite models by reduction to function-free clause logic

    • ...The incremental usage of the SAT solver follows [26, 32] as implemented in MiniSAT [33] and PicoSAT [11]...

    Robert Brummayeret al. Lemmas on Demand for the Extensional Theory of Arrays

Sort by: