path: root/proofs/signatures/drat.plf

; Deps: lrat.plf
;
; Implementation of DRAT checking.
;
; Unfortunately, there are **two** different notions of DRAT floating around in
; the world:
;   * Specified   DRAT : This is a reasonable proof format
;   * Operational DRAT : This is a variant of specified DRAT warped by the
;                        details of common SAT solver architectures.
;
; Both are detailed in this paper, along with their differences:
;   http://fmv.jku.at/papers/RebolaPardoBiere-POS18.pdf
;
; This signature contains implementations for a checker for each.
; **Specified DRAT** is first.

; A DRAT proof itself: a list of addition or deletion instructions.
(declare DRATProof type)
(declare DRATProofn DRATProof)
(declare DRATProofa (! c clause (! p DRATProof DRATProof)))
(declare DRATProofd (! c clause (! p DRATProof DRATProof)))

; ==================== ;
; Functional  Programs ;
; ==================== ;

; Are two clauses equal (i.e., if interpretted as sets of literals, are those
; sets equal?)
;
; Assumes that marks 1,2,3,4 are clear for the constituent variables, and
; leaves them clear afterwards.
;
; Since clauses are sets, it is insufficient to do list equality.
; We could sort them, but that would require defining an order on our variables,
; and incurring the cost of sorting.
;
;
; Instead, we do the following:
;  1. Sweep the first clause, marking variables with flags 1,3 (pos) and 2,4 (neg)
;  2. Sweep the second clause, erasing marks 1,2. Returning FALSE if no mark 3,4.
;  3. Unsweep the first clause, returning FALSE on marks 1,2.
;     Also unmarking 3,4, and 1,2 if needed
;
; So the mark 1 means (seen as + in c1, but not yet in c2)
;    the mark 3 means (seen as + in c1)
;    the mark 2 means (seen as - in c1, but not yet in c2)
;    the mark 4 means (seen as - in c1)
;
; This implementation **does not**:
;    1. assume that clauses do not have duplicates
;       (so the clause [x v x v ~y] is an accceptable input)
;    2. assume that clauses are non-tautological
;       (so the clause [x v ~x] is an acceptable input)
;
; TODO(aozdemir) This implementation could be further optimized b/c once c1 is
; drained, we need not continue to pattern match on it.
(program clause_eq ((c1 clause) (c2 clause)) bool
         (match
           c1
           (cln (match
                  c2
                  (cln tt)
                  ((clc c2h c2t) (match
                                   c2h
                                   ((pos v)
                                    (ifmarked1
                                      v
                                      (do (markvar1 v)
                                        (clause_eq c1 c2t))
                                      (ifmarked3
                                        v
                                        (clause_eq c1 c2t)
                                        ff)))
                                   ((neg v)
                                    (ifmarked2
                                      v
                                      (do (markvar2 v)
                                        (clause_eq c1 c2t))
                                      (ifmarked4
                                        v
                                        (clause_eq c1 c2t)
                                        ff)))))))
           ((clc c1h c1t) (match
                            c1h
                            ((pos v)
                             (ifmarked3
                               v
                               (clause_eq c1t c2)
                               (do (markvar3 v)
                                 (do (markvar1 v)
                                   (let res (clause_eq c1t c2)
                                     (do (markvar3 v)
                                       (ifmarked1
                                         v
                                         (do (markvar1 v) ff)
                                         res)))))))
                            ((neg v)
                             (ifmarked4
                               v
                               (clause_eq c1t c2)
                               (do (markvar4 v)
                                 (do (markvar2 v)
                                   (let res (clause_eq c1t c2)
                                     (do (markvar4 v)
                                       (ifmarked2
                                         v
                                         (do (markvar2 v) ff)
                                         res)))))))))))


; Does this formula contain bottom as one of its clauses?
(program cnf_has_bottom ((cs cnf)) bool
         (match cs
                (cnfn ff)
                ((cnfc c rest) (match c
                                      (cln tt)
                                      ((clc l c') (cnf_has_bottom rest))))))

; Return a new cnf with one copy of this clause removed.
; If the clause is absent, returns the original cnf.
(program cnf_remove_clause ((c clause) (cs cnf)) cnf
         (match cs
                (cnfn cnfn)
                ((cnfc c' cs')
                 (match (clause_eq c c')
                        (tt cs')
                        (ff (cnfc c' (cnf_remove_clause c cs')))))))

; return (c1 union (c2 \ ~l))
; Significant for how a RAT is defined.
(program clause_pseudo_resolvent ((c1 clause) (c2 clause)) clause
         (clause_dedup (clause_append c1
                                      (clause_remove_all
                                        (lit_flip (clause_head c1)) c2))))

; Given a formula, `cs` and a clause `c`, return all pseudo resolvents, i.e. all
;     (c union (c' \ ~head(c)))
;   for c' in cs, where c' contains ~head(c)
(program collect_pseudo_resolvents ((cs cnf) (c clause)) cnf
         (match cs
                (cnfn cnfn)
                ((cnfc c' cs')
                 (let rest_of_resolvents (collect_pseudo_resolvents cs' c)
                   (match (clause_contains_lit c' (lit_flip (clause_head c)))
                          (tt (cnfc (clause_pseudo_resolvent
                                      c
                                      c')
                                    rest_of_resolvents))
                          (ff rest_of_resolvents))))))

; =============================================================== ;
; Unit Propegation implementation (manipulates global assignment) ;
; =============================================================== ;
; See the lrat file for a description of the global assignment.

; The result of search for a unit clause in
(declare UnitSearchResult type)
; There was a unit, and
;    this is the (previously floating) literal that is now satisfied.
;    this is a version of the input cnf with satisfied clauses removed.
(declare USRUnit (! l lit (! f cnf UnitSearchResult)))
; There was an unsat clause
(declare USRBottom UnitSearchResult)
; There was no unit.
(declare USRNoUnit UnitSearchResult)

; If a UnitSearchResult is a Unit, containing a cnf, adds this clause to that
; cnf. Otherwise, returns the UnitSearchResult unmodified.
(program USR_add_clause ((c clause) (usr UnitSearchResult)) UnitSearchResult
         (match usr
                ((USRUnit l f) (USRUnit l (cnfc c f)))
                (USRBottom USRBottom)
                (USRNoUnit USRNoUnit)))

; Searches through the clauses, looking for a unit clause.
; Reads the global assignment. Possibly assigns one variable.
;  Returns
;    USRBottom     if there is an unsat clause
;    (USRUnit l f) if there is a unit, with lit l, and
;                  f is the cnf with some SAT clauses removed.
;    USRNoUnit     if there is no unit
(program unit_search ((f cnf)) UnitSearchResult
         (match f
                (cnfn USRNoUnit)
                ((cnfc c f')
                 (match (clause_check_unit_and_maybe_mark c)
                        (MRSat (unit_search f'))
                        ((MRUnit l) (USRUnit l f'))
                        (MRUnsat USRBottom)
                        (MRNotUnit (USR_add_clause c (unit_search f')))))))


; Given the current global assignment, does the formula `f` imply bottom via
; unit propegation? Leaves the global assignment in the same state that it was
; initially.
(program unit_propegates_to_bottom ((f cnf)) bool
         (match (unit_search f)
                (USRBottom tt)
                ((USRUnit l f') (let result (unit_propegates_to_bottom f')
                               (do (lit_un_mk_sat l)
                                 result)))
                (USRNoUnit ff)))

; ================================== ;
; High-Level DRAT checking functions ;
; ================================== ;

; Is this clause an AT?
(program is_at ((cs cnf) (c clause)) bool
         (match (is_t c)
                (tt tt)
                (ff (do (clause_mk_all_unsat c)
                      (let r (unit_propegates_to_bottom cs)
                        (do (clause_un_mk_all_unsat c)
                          r))))))

; Are all of these clauses ATs?
(program are_all_at ((cs cnf) (clauses cnf)) bool
         (match clauses
                (cnfn tt)
                ((cnfc c clauses')
                 (match (is_at cs c)
                        (tt (are_all_at cs clauses'))
                        (ff ff)))))

; Is the clause `c` a RAT for the formula `cs`?
(program is_rat ((cs cnf) (c clause)) bool
         (match (is_t c)
                (tt tt)
                (ff (match (is_at cs c)
                           (tt tt)
                           (ff (match c
                                      (cln ff)
                                      ((clc a b) (are_all_at ; dedent
                                 cs
                                 (collect_pseudo_resolvents cs c)))))))))

; Is this proof a valid DRAT proof of bottom?
(program is_specified_drat_proof ((f cnf) (proof DRATProof)) bool
         (match proof
                (DRATProofn (cnf_has_bottom f))
                ((DRATProofa c p) (match
                                    (is_rat f c)
                                    (tt (is_specified_drat_proof (cnfc c f) p))
                                    (ff ff)))
                ((DRATProofd c p)
                 (is_specified_drat_proof (cnf_remove_clause c f) p))))


; =============================== ;
; Operational DRAT implementation ;
; =============================== ;

; Operation DRAT is defined in the paper "Two Flavors of DRAT".
; Below is an extension of the DRAT signature to handle it.

; Notes on types.
; For operational DRAT it is useful to manifest partial assignments in values
; (although we still use the global assignment in some places). To this end,
; literals are used to represent single-variable assignments ((pos v) denotes
; {v maps to true}) and clauses are partial assignments by way of being
; literal lists.

; Copy the partial assignment represented by a clause into the global
; assignment. Fails if that clause represents an inconsistent partial
; assignment (e.g. v is both true and false)
(program clause_into_global ((a clause)) Unit
         (match a
                (cln unit)
                ((clc l rest)
                 (do (lit_mk_sat l) (clause_into_global rest)))))

; Remove the partial assignment represented by c from the global assignment
(program clause_undo_into_global ((a clause)) Unit
         (match a
                (cln unit)
                ((clc l rest)
                 (do (lit_un_mk_sat l) (clause_undo_into_global rest)))))

; Does this clause have no floating literals w.r.t. the global assignment?
(program clause_no_floating ((c clause)) bool
         (match c
                (cln tt)
                ((clc l rest) (match (lit_is_floating l)
                                    (tt ff)
                                    (ff (clause_no_floating rest))))))

; Does this clause have no sat literals w.r.t. the global assignment?
(program clause_no_sat ((c clause)) bool
         (match c
                (cln tt)
                ((clc l rest) (match (lit_is_sat l)
                                    (tt ff)
                                    (ff (clause_no_sat rest))))))

; Does this clause have one sat literal w.r.t. the global assignment?
(program clause_one_sat ((c clause)) bool
         (match c
                (cln ff)
                ((clc l rest) (match (lit_is_sat l)
                                    (tt (clause_no_sat rest))
                                    (ff (clause_one_sat rest))))))

; Is this clause a unit clause w.r.t. the global assignment?
; This notion is defined as:
;    * A clause where no literals are floating, and exactly one is sat.
(program clause_is_unit_wrt_up_model ((c clause) (up_model clause)) bool
         (let c' (clause_dedup c)
         (do (clause_into_global up_model)
           (let result (match (clause_no_floating c')
                              (tt (clause_one_sat c'))
                              (ff ff))
             (do (clause_undo_into_global up_model)
               result)))))

; Result from constructing a UP model (defined in "Two Flavors of DRAT")
; Technically, we're constructing the shared UP model -- the intersection of all
; UP models.
; Informally, this is just the partial assignment implied by UP.
;
; This type is necessary, because constructing a UP model can reveal an
; inconsistent UP model -- one which assigns some variable to true and false.
; This would break our machinery, so we special case it.
(declare UPConstructionResult type)
; An actual model
(declare UPCRModel (! up_model clause UPConstructionResult))
; Bottom is implied!
(declare UPCRBottom UPConstructionResult)


; Do unit propagation on `f`, constructing a UP model for it.
(program build_up_model ((f cnf)) UPConstructionResult
         (match (unit_search f)
                (USRBottom UPCRBottom)
                (USRNoUnit (UPCRModel cln))
                ((USRUnit l f')
                 (let result (build_up_model f')
                   (do (lit_un_mk_sat l)
                     (match result
                            (UPCRBottom UPCRBottom)
                            ((UPCRModel model) (UPCRModel (clc l model)))))))))

; Given some starting assignment (`up_model`), continue UP to construct a larger
; model.
(program extend_up_model ((f cnf) (up_model clause)) UPConstructionResult
         (do (clause_into_global up_model)
           (let result (build_up_model f)
             (do (clause_undo_into_global up_model)
               (match result
                      (UPCRBottom UPCRBottom)
                      ((UPCRModel up_model')
                       (UPCRModel (clause_append up_model up_model'))))))))

; Helper for `is_operational_drat_proof` which takes a UP model for the working
; formula. The UP model is important for determining which clause deletions
; actually are executed in operational DRAT. Passing the UP model along
; prevents it from being fully recomputed every time.
(program is_operational_drat_proof_h ((f cnf) (up_model clause) (pf DRATProof)) bool
         (match pf
                (DRATProofn (cnf_has_bottom f))
                ((DRATProofd c pf')
                 (match (clause_is_unit_wrt_up_model c up_model)
                        (tt (is_operational_drat_proof_h f up_model pf'))
                        (ff (is_operational_drat_proof_h
                              (cnf_remove_clause c f) up_model pf'))))
                ((DRATProofa c pf')
                 (let f' (cnfc c f)
                   (match (is_rat f c)
                          (tt (match (extend_up_model f' up_model)
                                     (UPCRBottom tt)
                                     ((UPCRModel up_model')
                                      (is_operational_drat_proof_h f' up_model' pf'))))
                          (ff ff))))))

; Is this an operational DRAT proof of bottom for this formula?
(program is_operational_drat_proof ((f cnf) (pf DRATProof)) bool
         (match (build_up_model f)
                (UPCRBottom tt)
                ((UPCRModel model) (is_operational_drat_proof_h f model pf))))

; Is this a specified or operational DRAT proof of bottom for this formula?
(program is_drat_proof ((f cnf) (pf DRATProof)) bool
         (match (is_specified_drat_proof f pf)
                (tt tt)
                (ff (is_operational_drat_proof f pf))))

(declare drat_proof_of_bottom
         (! f cnf
            (! proof_of_formula (cnf_holds f)
               (! proof DRATProof
                  (! sc (^ (is_drat_proof f proof) tt)
                     bottom)))))