(*
Copyright (c) 2013-2014, Simon Cruanes
All rights reserved.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions are met:
Redistributions of source code must retain the above copyright notice, this
list of conditions and the following disclaimer. Redistributions in binary
form must reproduce the above copyright notice, this list of conditions and the
following disclaimer in the documentation and/or other materials provided with
the distribution.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*)
(** {1 Simple Resolution Prover} *)
module Err = CCError
module T = Logtk.FOTerm
module F = Logtk.Formula.FO
module Substs = Logtk.Substs
module Unif = Logtk.Unif
module Util = Logtk.Util
(** Global signature (maps symbols such as "f", "parent_of" or "greater"
to their type). Every symbol has exactly one type.
The initial signature is the TPTP signature (logic connectives) *)
let _signature = ref Logtk.Signature.TPTP.base
(** We do not have to do anything about terms, because they are already
defined in {! Logtk.FOTerm}. Terms are either variables or
applications of a constant (symbol) to a list of sub-terms.
Examples (capitalized letter are variables):
- f(X, g(X,a))
- age_of(grandmother_of(frida))
- Y
- the_universe
*)
(** {2 Literals and Clauses} *)
(** A literal is an atomic proposition (term of type [$o], i.e. the type of
propositions), or its negation. We represent this as a pair of [(term, sign)].
Examples:
- [(older_than(obama, bieber), true)]
- [(lives_in(paris, poutine), false)]
*)
module Lit = struct
type t = T.t * bool
(** We also define a few basic comparison and printing functions.
Comparison functions are used by many data structures;
Printing is useful for informing the user of results or
for debugging. *)
let compare = CCOrd.pair T.cmp CCOrd.bool_
let equal a b = compare a b=0
let pp buf (t,b) = Printf.bprintf buf "%s%a" (if b then "" else "¬") T.pp t
end
(** A clause is a disjunction ("or") of literals. We simply use a list
of literals.
Example:
[ (lives_in(paris, X), false); (eats_baguette(X), true) ]
(means "forall X, if X lives in paris then X eats baguette")
*)
module Clause = struct
type t = Lit.t list
let make l = CCList.Set.uniq ~eq:Lit.equal l
let compare = CCOrd.list_ Lit.compare
let equal a b = compare a b = 0
(** A clause is trivial if it contains both a literal and its opposite.
It means the clause is tautological, that is, always true; we can
dispose of it because resolution is about {b refutation} (proving false) *)
let is_trivial c =
List.exists
(fun (t,b) ->
b &&
List.exists (fun (t',b') -> not b' && T.eq t t') c
) c
(** A substitution maps some variables to terms. Here this function will
be used to {i apply} the substitution to a clause - replace
variables of the clause by their image in the substitution (or keep
them unchanged if they do not appear in the substitution.
Substitutions are pre-defined in Logtk, and applying a substitution
to a term is defined too (the function {!Subst.FO.apply} that
applies a substitution to a first-order term)
*)
let apply_subst ~renaming subst c s_c =
make (List.map (fun (t,b) -> Substs.FO.apply ~renaming subst t s_c, b) c)
(** printing a clause: print literals separated with "|" *)
let pp buf c = CCList.pp ~sep:" | " Lit.pp buf c
(** Conversion from list of atomic formulas.
type: [Formula.t list -> clause] *)
let _of_forms c =
let _atom f = match F.view f with
| F.Not f' ->
begin match F.view f' with
| F.Atom t -> t,false
| _ -> failwith (CCPrint.sprintf "unsupported formula %a" F.pp f)
end
| F.Atom t -> t, true
| _ -> failwith (CCPrint.sprintf "unsupported formula %a" F.pp f)
in
make (List.map _atom c)
end
(** A pair (clause, index) where the index refers to some literal
in the clause. *)
module ClauseWithPos = struct
type t = Clause.t * int
let compare = CCOrd.pair Clause.compare CCInt.compare
end
(** {2 Saturation Algorithm} *)
(** An Index is a multimap from terms to (clause,index). Basically
when we process a clause [c], for each literal [(term,sign)]
at position [i] in the clause [c], we add
[term -> (c, i)] into the index. Later we will be able to retrieve
the pair [(c,i)] using any term that {i unifies} with [term]. *)
module Index = Logtk.NPDtree.MakeTerm(ClauseWithPos)
(** Set of clauses. Easy to define thanks to {!Clause.compare} *)
module ClauseSet = Set.Make(Clause)
(** State for one proof:
- One term index (maps terms to the pairs [(clause, index of literal)]
they appear in);
- One set of processed ("active") clauses;
- One queue of clauses yet to be processed. We process those clauses
one by one.
*)
let _idx = ref (Index.empty())
let _active_set = ref ClauseSet.empty
let _passive_set = Queue.create()
exception Unsat
(** Raise this exception when the empty clause (i.e., "false")
is found. This means the original clause set implies false
and therefore that it's absurd. *)
(** add [c] to the passive set, if not already present in
the active set nor it is trivial. *)
let _add_passive c =
if c = [] then raise Unsat
else if Clause.is_trivial c
then (
Util.debug 4 "clause %a is trivial" Clause. pp c;
)
else if not (ClauseSet.mem c !_active_set)
then (
Util.debug 4 "new passive clause %a" Clause.pp c;
Queue.push c _passive_set
)
(** When we process a clause [c], we put it into the active set
(set of processed clauses). That also means every literal [(term,sign)]
at index [i] will go into the index, so we can retrieve [c]
by its literals later.
*)
let _add_active c =
_active_set := ClauseSet.add c !_active_set;
List.iteri
(fun i (t,_) -> _idx := Index.add !_idx t (c,i))
c
(** Factoring inference (takes one clause and deduce other clauses):
{[
A or A' or C
---------------
sigma (A' or C)
if sigma(A) = sigma(A')
]}
means that if the clause has two positive literals (A,true) and (A',true)
with some substitution sigma such that sigma(A)=sigma(A'), then
we can {i factor} those literals into (sigma(A),true) provided
we also apply sigma to the rest of the clause.
*)
let _factoring c =
List.iteri
(fun i (t,b) ->
if b then List.iteri
(fun j (t',b') ->
(** Only try the inference if the two literals have positive sign.
The restriction [i < j] is used not to do the same inference
twice (symmetry).
*)
if i %a" Clause.pp c Clause.pp c';
(** New clauses go into the passive set *)
_add_passive c'
with Unif.Fail -> ()
) c
) c
(** Resolution inference rule, between the clause [C] and any clause [D]
from the active set.
{[
A or C ¬A' or D
------------------
sigma(C or D)
if sigma(A) = sigma(A')
]}
This rule is called "resolution" and it's one of the first automated proof
technique ever. If "resolves" together two complementary literals in
two clauses (assuming those clauses do not share variables).
Let us explain in the propositional case (ignoring variables), assuming
[A = A']. The idea is, roughly:
- we know that either [A] or either [not A] is true
(excluded middle)
- if [A] is true, it means that [not A' or D]
can only be true if [D] is true (since [A=A'=true]). Therefore
[D] must be true.
- if [A] is false, then [A or C] can only be true if [C] is true;
therefore [C] holds.
- by excluded middle one of those must be true, so in any
case [C or D] is true. Hence the conclusion.
For the first-order case, we compute the {b most general unifier} or
[A] and [A'] (if it exists), call this unifier substitution [sigma].
Then, the reasoning is the same as in the propositional case since
the literals are actually equal.
Note: the "0" and "1" are {b scopes}, a trick I use to avoid actually
renaming variables in one of the clauses. More details can be found
in the documentation for {!Substs} or in the talk I (Simon) gave at PAAR
2014.
*)
let _resolve_with c =
List.iteri
(fun i (t,b) ->
(** Retrieve within the index, mappings [term -> (clause,index)]
such that [term] unifies with [t]. 0 and 1 are again scopes. *)
Index.retrieve_unifiables !_idx 0 t 1 ()
(fun () _t' (d,j) subst ->
let (_,b') = List.nth d j in
(** We have found [_t'], and a pair [(d, j)] such
that [d] is another clause, and the [j]-th literal of [d]
begin [_t', b']).
If [b] and [b'] are complementary we are in the case where
resolution applies.
*)
if b<>b'
then (
let renaming = Substs.Renaming.create() in
(** Build the conclusion clause, merging the remainders [c']
and [d'] (which live respectively in scope 1 and 0)
of the clauses together after applying the substitution. *)
let concl =
(let c' = CCList.Idx.remove c i in
Clause.apply_subst ~renaming subst c' 1)
@
(let d' = CCList.Idx.remove d j in
Clause.apply_subst ~renaming subst d' 0)
in
(** Simplify the resulting clause (remove duplicate literals)
and add it into the passive set, to be processed later *)
let concl = Clause.make concl in
Util.debug 3 "resolution of %a and %a ---> %a"
Clause.pp c Clause.pp d Clause.pp concl;
_add_passive concl
)
)
) c
(** Main saturation algorithm, a simple "given clause" loop. This is
the outer loop of the resolution procedure: given an initial
set of [clauses], the algorithm does:
- add all the clauses into the passive set
- while some passive clauses remain unprocessed, pick one of them,
call it [c], and then do the following:
- add [c] into the active set
- perform inferences between [c] and the active set (including [c] itself)
- add the resulting new clauses to the passive set.
- if at any point the empty clause [[]] is found, then
the initial set of clauses is unsatisfiable (absurd).
- otherwise, if the loop stops, we have computed a fixpoint of the
initial clauses with respect to inferences without finding [false],
which means the original set of clauses is satisfiable (admits a model) *)
let _saturate clauses =
List.iter _add_passive clauses;
try
while not (Queue.is_empty _passive_set) do
let c = Queue.pop _passive_set in
(** Is the clause [c] suitable for processing? It must not be processed
yet and must not be trivial either. *)
if not (Clause.is_trivial c) && not (ClauseSet.mem c !_active_set)
then (
Util.debug 2 "given clause: %a" Clause.pp c;
_add_active c;
_resolve_with c;
_factoring c;
)
done;
`Sat
with
| Unsat -> `Unsat
(** {2 Main} *)
(** Read the problem to solve from the file [f], (try to) solve it
and return the result. We use an error monad to make error
handling easier (the function [>>=] is a {i monadic bind}). *)
let process_file f =
Util.debug 2 "process file %s..." f;
let res = Err.(
(** parse the file in the TPTP format *)
Logtk_parsers.Util_tptp.parse_file ~recursive:true f
(** Perform type inference and type checking (possibly updating
the signature) *)
>>= Logtk_parsers.Util_tptp.infer_types (`sign !_signature)
(** CNF ("clausal normal form"). We transform arbitrary first order
formulas into a set of clauses (see the {!Clause} module)
because resolution only works on clauses.
This algorithm is already implemented in {!Logtk}. *)
>>= fun (signature, statements) ->
let clauses = Logtk_parsers.Util_tptp.Typed.formulas statements in
let clauses = Sequence.to_list clauses in
(** A way to create fresh symbols for {i Skolemization} *)
let ctx = Logtk.Skolem.create ~prefix:"sk" signature in
let clauses = Logtk.Cnf.cnf_of_list ~ctx clauses in
let clauses = CCList.map Clause._of_forms clauses in
_signature := Logtk.Skolem.to_signature ctx; (* recover signature *)
(** Perform saturation (solve the problem) *)
Err.return (_saturate clauses)
) in
match res with
| `Error msg ->
print_endline msg;
exit 1
| `Ok `Sat -> print_endline "sat"
| `Ok `Unsat -> print_endline "unsat"
(** Parse command-line arguments, including the file to process *)
let _options = ref (
[
] @ Logtk.Options.global_opts
)
let _help = "usage: resolution file.p"
let _file = ref None
let _set_file f = match !_file with
| None -> _file := Some f
| Some _ -> failwith "can only deal with one file"
let main () =
Arg.parse !_options _set_file _help;
match !_file with
| None -> print_endline _help; exit 0
| Some f -> process_file f
let () = main()