From 42f8d0aafe79d67517094751b3234f04ac145a60 Mon Sep 17 00:00:00 2001 From: Laurent Orseau Date: Fri, 5 Mar 2021 14:23:44 +0000 Subject: [PATCH] Internal PiperOrigin-RevId: 361132516 --- satore/Clause.rkt | 4 ++++ satore/README.md | 29 ++++++++++++------------ satore/examples/socrates.p | 4 ++-- satore/interact.rkt | 2 -- satore/rewrite-tree.rkt | 2 +- satore/saturation.rkt | 24 +++++++++++++++----- satore/tests/saturation.rkt | 44 +++++++++++++++++++++++------------- satore/tests/timeplus.rkt | 13 ----------- satore/tests/unification.rkt | 16 +++++++++++++ satore/unification-tree.rkt | 12 +++++----- satore/unification.rkt | 28 +++++++++++++++++++---- 11 files changed, 114 insertions(+), 64 deletions(-) delete mode 100644 satore/tests/timeplus.rkt diff --git a/satore/Clause.rkt b/satore/Clause.rkt index 3a4abf2..1dbedd1 100644 --- a/satore/Clause.rkt +++ b/satore/Clause.rkt @@ -309,6 +309,10 @@ (provide Clausify check-Clause-set-equivalent?) + ;; Takes a symbol tree, turns symbol variables into actual `Var`s, freshes them, + ;; sorts the literals and makes a new Clause. + ;; + ;; tree? -> Clause? (define Clausify (compose make-Clause clausify)) ;; Returns whether for every clause of Cs1 there is an α-equivalent clause in Cs2. diff --git a/satore/README.md b/satore/README.md index 555b8ff..f22af7b 100644 --- a/satore/README.md +++ b/satore/README.md @@ -1,6 +1,6 @@ -# Satore: First-order logic saturation with atomic rewriting +# Satore: First-order logic saturation with atom rewriting -This is a first-order logic resolution based theorem prover in CNF without +Satore is a first-order logic resolution based theorem prover in CNF without equality, but with atom rewrite rules. New rewrite rules can be discovered during the proof search, potentially reducing exponentially the search space. @@ -9,25 +9,26 @@ Satore stands for Saturation with Atom Rewriting. ## Installation -### Install racket (Apache2/MIT): -* Windows, MacOS X: https://download.racket-lang.org -* Ubuntu/Debian: `[sudo] apt install racket` -* Linux (other): [Download](https://download.racket-lang.org) the `.sh` and - install it with `[sudo] sh racket-.sh` +First, install the **Racket** programming language (Apache2/MIT): +https://download.racket-lang.org -You may need to configure the PATH environment variable to include the -directory containing the `racket` and `raco` executables. -For Windows this directory should be something like -`C:>Program Files\Racket`. +Note for Linux users: Do read the comments on the download page. -### Install satore and its dependencies (all are Apache2/MIT licensed): +You may need to +[configure the PATH environment variable](https://github.com/racket/racket/wiki/Set-your-PATH-environment-variable) +to include the directory containing the `racket` and `raco` executables. -In a directory of your choice, type: +To install **satore** and its dependencies (all are Apache2/MIT licensed), +in a directory of your choice, type: ```shell git clone https://github.com/deepmind/deepmind-research/tree/master/satore -raco pkg install --auto --link satore +raco pkg install --auto --update-deps --link satore ``` + ## Running Satore diff --git a/satore/examples/socrates.p b/satore/examples/socrates.p index ef3df55..eea419e 100644 --- a/satore/examples/socrates.p +++ b/satore/examples/socrates.p @@ -1,3 +1,3 @@ cnf(humans_are_mortal, axiom, (~human(X) | mortal(X))). -cnf(socrates_is_human, hypothesis, (human(c))). -cnf(socrates_is_mortal, negated_conjecture, (~mortal(c))). +cnf(socrates_is_human, hypothesis, (human(socrates))). +cnf(socrates_is_mortal, negated_conjecture, (~mortal(socrates))). diff --git a/satore/interact.rkt b/satore/interact.rkt index d3e038f..a1306ad 100644 --- a/satore/interact.rkt +++ b/satore/interact.rkt @@ -17,8 +17,6 @@ ;; variables set via the (list 'var val) pattern are set in the main namespace. ;; Even though the namespace is at the module level, the variables ;; are set in the namespace with their value so they can be used with eval. -;; TODO: When a ns-anchor is given, commands are eval'ed by default, and to directly modify -;; TODO: variables one must use ! (where the second argument is evaled) (define-syntax (interact stx) (syntax-parse stx #:literals (list) diff --git a/satore/rewrite-tree.rkt b/satore/rewrite-tree.rkt index 0e58ed4..0e90031 100644 --- a/satore/rewrite-tree.rkt +++ b/satore/rewrite-tree.rkt @@ -749,7 +749,7 @@ (define to-lit2 (rule-to-literal rl2)) (define s (unify lnot-from-lit1 from-lit2)) (when s - (define cl (clausify (substitute (list to-lit1 to-lit2) s))) + (define cl (clause-normalize (substitute (list to-lit1 to-lit2) s))) (define C (make-Clause cl (list (rule-Clause rl) (rule-Clause rl2)) #:type 'c-p)) ; critical-pair (define max-size (max (literal-size (rule-from-literal rl)) diff --git a/satore/saturation.rkt b/satore/saturation.rkt index 41c25ba..3a30de3 100644 --- a/satore/saturation.rkt +++ b/satore/saturation.rkt @@ -69,12 +69,17 @@ '(weight-fair weight) "Cost type.") +(define-global *cost-depth-factor* 1.5 + "Cost = weight + cost-depth-factor * depth" + (λ (x) #true) + string->number) + (define-global *cost-noise* 0. "Noise factor to add to costs" (λ (x) (and (real? x) (>= x 0))) string->number) -(define-global:boolean *parent-discard?* #true +(define-global:boolean *parent-discard?* #false "Discard clauses when at least one parent has been discarded?") (define-global:boolean *discover-online?* #true @@ -224,7 +229,7 @@ (set-Clause-cost! C (if (empty? (Clause-clause C)) -inf.0 ; empty clause should always be top of the list - (+ (* (Clause-depth C) 1.5) + (+ (* (Clause-depth C) (*cost-depth-factor*)) (Clause-size C)))))]) ;; Add noise to the cost so as to potentially solve more later. @@ -363,7 +368,7 @@ (define step 0) (reset-n-tautologies!) - (define n-parent-pruning 0) + (define n-parent-discard 0) (define n-forward-subsumed 0) (define n-backward-subsumed 0) (reset-n-binary-rewrites!) @@ -390,7 +395,7 @@ (subsumes-checks . ,n-subsumes-checks) (subsumes-steps . ,n-subsumes-steps) (subsumes-breaks . ,n-subsumes-breaks) - (parent-pruning . ,n-parent-pruning) + (parent-discard . ,n-parent-discard) (L-resolvent-pruning . ,n-L-resolvent-pruning) (memory . ,(current-memory-use)) ; doesn't account for GC---this would take too much time (time . ,(- stop-time start-time)) @@ -486,7 +491,7 @@ [(and parent-discard? (ormap Clause-discarded? (Clause-parents selected-Clause))) (when-debug>= steps (displayln "At least one parent has been discarded. Discard too.")) (discard-Clause! selected-Clause) - (++ n-parent-pruning) + (++ n-parent-discard) (loop)] #:else (set-Clause-candidate?! selected-Clause #false) @@ -616,6 +621,10 @@ #:rewriter (λ (C) (binary-rewrite-Clause rwtree C)) #:L-resolvent-pruning? L-resolvent-pruning-allowed?))) + (when-debug>= interact + (displayln "New candidates:") + (print-Clauses new-Candidates)) + ;; If a clause has no resolvent with the active set (when complete) ;; then it will never resolve with anything and can thus be discarded. #:cond @@ -877,6 +886,8 @@ (define clauses (tptp-prog->clauses tptp-program)) (define quiet? (*quiet-json?*)) + (define n-rules-init (rewrite-tree-count rwtree-in)) + (let loop ([iter 1] [uncapped-current-cpu-limit cpu-first-limit] [rwtree-in rwtree-in]) (define remaining-cpu (- cpu-limit (- (current-inexact-seconds) cpu-start))) (define current-cpu-limit (min remaining-cpu uncapped-current-cpu-limit)) @@ -887,7 +898,8 @@ current-cpu-limit)) ; Simplify the set of rules (only once) - (begin ; unless (= 1 iter) ; don't do this if no restarting + (unless (and (= 1 iter) + (= 0 n-rules-init)) ; don't do this if no restarting ; Note that these steps destroy the Clause ancestry, and proofs will be incomplete. (unless quiet? (printf "; Rules stats: ~v\n" (rewrite-tree-stats rwtree-in)) diff --git a/satore/tests/saturation.rkt b/satore/tests/saturation.rkt index d33b264..d36400f 100644 --- a/satore/tests/saturation.rkt +++ b/satore/tests/saturation.rkt @@ -58,12 +58,13 @@ ; encapsulated to avoid collisions (let () body ...)))) -(for-in-list* ([l-res-pruning? #true #false] - [neg-lit-select? #true #false] - [atom<=> KBO1lex<=> atom1<=>] - [dynamic-ok? #true #false] - [rwtree-in=out? #true #false] ; false means no search for new rules - ;#:unless (and l-res-pruning? neg-lit-select?) ; can't have both at the same time +(for-in-list* ([neg-lit-select? #true #false] + [l-res-pruning? #true #false] + [atom<=> #false KBO1lex<=> atom1<=>] + [dynamic-ok? #;#true #false] + [parent-discard? #false] + ; notice: if parent-discard? is #true, then can't have both rewriting and + ; neg-lit-select. ) (define-wrapper (saturation @@ -73,10 +74,11 @@ #:? [cpu-limit (*cpu-limit*)] ; in seconds #:? [rwtree (make-rewrite-tree #:atom<=> atom<=> #:dynamic-ok? dynamic-ok?)] - #:? [rwtree-out (and rwtree-in=out? rwtree)] + #:? [rwtree-out (and atom<=> rwtree)] #:? backward-rewrite? #:? age:cost #:? cost-type + #:? [parent-discard? parent-discard?] #:? [disp-proof? #false] #:? [L-resolvent-pruning? l-res-pruning?] #:? [negative-literal-selection? neg-lit-select?])) @@ -86,7 +88,7 @@ (check-equal? (dict-ref res 'L-resolvent-pruning) 0)) (unless dynamic-ok? (check-equal? (dict-ref res 'binary-rules-dynamic) 0)) - (unless rwtree-in=out? + (unless atom<=> (check-equal? (dict-ref res 'binary-rules) 0) (check-true (= (dict-ref res 'binary-rewrites) 0))) res) @@ -142,7 +144,6 @@ - ; TPTP 100k idx = 348 (check-equal? (dict-ref (saturation (Vars+clausify-list '( [(big_f T0_0 T0_1) (big_g T0_0 T0_2)] @@ -153,7 +154,6 @@ 'refuted) - ; TPTP 100k idx = 784 (check-equal? (dict-ref (saturation (Vars+clausify-list '( [p1 p2] [p1 (not p2)] @@ -162,8 +162,20 @@ 'status) 'refuted) + (check-equal? + (dict-ref (saturation + '((p1 p2 p3) + (p1 p3 (not p2)) + (p2 p3 (not p1)) + (p1 p2 (not p3)) + (p1 (not p2) (not p3)) + (p2 (not p1) (not p3)) + (p3 (not p1) (not p2)) + ((not p1) (not p2) (not p3)))) + 'status) + 'refuted) + - ; TPTP 100k idx = 117 (check-equal? (dict-ref (saturation (Vars+clausify-list @@ -230,7 +242,7 @@ ((not (s D d))) )))) (check-equal? (dict-ref res 'status) 'refuted) - (when rwtree-in=out? + (when atom<=> (check > (dict-ref res 'unit-rules) 0) (check-equal? (dict-ref res 'binary-rules) 2) (check > (dict-ref res 'binary-rewrites) 0))) @@ -250,7 +262,7 @@ [(not (remove-me X y))] ; defeats urw )))) (check-equal? (dict-ref res 'status) 'refuted) - (when rwtree-in=out? + (when atom<=> (check-equal? (dict-ref res 'binary-rules) 4) (check-true (> (dict-ref res 'binary-rewrites) 0)))) ;; TODO: Same test but with rules loaded from a file @@ -275,7 +287,7 @@ [(not (remove-me X y))] ; defeats urw )))) (check-equal? (dict-ref res 'status) 'refuted) - (when rwtree-in=out? + (when atom<=> (check-equal? (dict-ref res 'binary-rules) 6) (check-true (> (dict-ref res 'binary-rewrites) 0)))) @@ -298,7 +310,7 @@ [(not (remove-me X y))] ; defeats urw )))) (check-equal? (dict-ref res 'status) 'refuted) - (when rwtree-in=out? + (when atom<=> (check-equal? (dict-ref res 'binary-rules) 6) (check-true (> (dict-ref res 'binary-rewrites) 0)))) @@ -323,6 +335,6 @@ [(not (remove-me X y))] ; defeats urw )))) (check-equal? (dict-ref res 'status) 'refuted) - (when rwtree-in=out? + (when atom<=> (check-equal? (dict-ref res 'binary-rules) 8) (check-true (> (dict-ref res 'binary-rewrites) 0))))) diff --git a/satore/tests/timeplus.rkt b/satore/tests/timeplus.rkt deleted file mode 100644 index 1efc6a7..0000000 --- a/satore/tests/timeplus.rkt +++ /dev/null @@ -1,13 +0,0 @@ -#lang racket/base - -(require "../timeplus.rkt" - rackunit) - -(check-equal? (string-drop-common-prefix '("auiebépo" "auiensrt" "au")) - '("iebépo" "iensrt" "")) -(check-equal? (string-drop-common-prefix '("auiebépo" "auiensrt" )) - '("bépo" "nsrt")) -(check-equal? (string-drop-common-prefix '("auiebépo" )) - '("")) -(check-equal? (string-drop-common-prefix '("" )) - '("")) diff --git a/satore/tests/unification.rkt b/satore/tests/unification.rkt index b606b64..445fad1 100644 --- a/satore/tests/unification.rkt +++ b/satore/tests/unification.rkt @@ -1,8 +1,10 @@ #lang racket/base (require (submod bazaar/order test) + racket/list racket/match rackunit + satore/clause satore/unification) (define (subst/#false->imsubst s) @@ -363,6 +365,20 @@ t) '([x . (f A B)]))) +(let ([c1 (clausify '((theorem (or A B)) (not (theorem (or A (or (or A B) B))))))] + [c2 (clausify '((theorem (or (_not_ A) (or B A)))))]) + (define s1 (unify (first c2) (lnot (second c1)))) + (define s2 (unify (lnot (second c1)) (first c2))) + (list c1 + c2 + s1 + (substitute (first c1) s1) + s2 + (substitute (first c1) s2)) + (check clause-equivalence? + (substitute (list (first c1)) s1) + (substitute (list (first c1)) s2))) + ;; Stress test for unification ;; This should take 0ms ;; See https://en.wikipedia.org/wiki/Unification_(computer_science) diff --git a/satore/unification-tree.rkt b/satore/unification-tree.rkt index c9f7a74..8e2f00a 100644 --- a/satore/unification-tree.rkt +++ b/satore/unification-tree.rkt @@ -4,13 +4,13 @@ ;**** Unification Tree ****; ;**************************************************************************************; -;;; A trie specialized for unifying literals. -;;; This is *different* from "substitution trees" +;;; An imperfect discrimination tree specialized for unifying literals and other +;;; operations. This is *different* from "substitution trees" ;;; (https://link.springer.com/chapter/10.1007%2F3-540-59200-8_52) -;;; TODO: This should be probably named a Clause-trie instead, since the -;;; TODO: major difference with the trie is that we are dealing with Clauses, which -;;; TODO: are lists of literals, and the same Clause can appear in different leaves -;;; TODO: of the trie. Unification is only one of the operations performed on Clauses. +;;; Note: This should be probably named a Clause-trie instead, since the +;;; major difference with the trie is that we are dealing with Clauses, which +;;; are lists of literals, and the same Clause can appear in different leaves +;;; of the trie. Unification is only one of the operations performed on Clauses. (require bazaar/cond-else bazaar/debug diff --git a/satore/unification.rkt b/satore/unification.rkt index 1feeae4..13cb393 100644 --- a/satore/unification.rkt +++ b/satore/unification.rkt @@ -629,17 +629,37 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even ;; Also, it's not necessary. (define reduce-mgu? #false) +;; Returns a term where the substitution s is applied to the term t. +;; The substitution `s` may not be 'reduced' in the sense that variables +;; of the domain may appear in the range. +;; +;; term? subst? -> term? +(define (substitute/slow t s) + (define t-orig t) + (let loop ([t t]) + (cond + [(null? t) t] + [(pair? t) + (cons (loop (car t)) + (loop (cdr t)))] + [(and (Var? t) + (subst-ref s t #false)) + ; Recur into the substitution. + => loop] + [else t]))) + ;; A simple box to signify that there is no need to attempt to substitute ;; inside `term` as this has already been done. (struct already-substed (term) #:prefab) -;; Returns a term where the substitution s is applied to the term t. -;; The substitution `s` may not be 'reduced' in the sense that variables -;; of the domain may appear in the range. +;; Like `substitute/slow` but avoids unnecessary work. ;; Such substitutions are performed 'on-demand', if needed. ;; Once a substitution has been applied recursively to a rhs, the resulting ;; term is marked with `already-substed` to avoid attempting it again. ;; +;; Notice: This function can only be used if `s` is *not* going to be extended, +;; otherwise it may not produce the correct result. +;; ;; term? subst? -> term? (define (substitute t s) (define t-orig t) @@ -678,7 +698,7 @@ For simplicity, we sometimes use 'term' to mean 'atom or term', or even ;; ;; Var? term? subst? -> (or/c #false subst?) (define (occurs?/extend V t2 subst) - (define t2c (substitute t2 subst)) + (define t2c (substitute/slow t2 subst)) (if (occurs? V t2c) #false (begin