aehyvari
commented
4 years ago The results on the initial implementation with a naive method of determining the satisfiability of a clause are inconclusive. To me it looks like there is a small positive effect when measuring the number of decisions. I ran some tests for QF_LRA:
- run time comparison noghost_vs_ghost-swap.pdf
- decision comparison noghost_vs_ghost-swap_decs.pdf
- average decision time comparison noghost_vs_ghost-swap_avg_dec_time.pdf
Note that there's a resolution problem with the avg dec time comparison and one dot corresponds therefore to many instances. For a proper analysis we'd have to go and see the "weight" of the dots.
I would try to see if a better clause satisfiability check will help with the run time, and otherwise keep this code disabled for now at least for QF_LRA, possibly enabling it for presumably more costly logics such as QF_LIA. QF_UF needs still to be tested.
blishko
An SMT formula $f$ in CNF is satisfiable if a theory-consistent partial truth assignment $p$ satisfies all clauses of $f$ (Prop. 2.2 of [1]). However, OpenSMT currently determines that an instance satisfiable only after finding a complete theory-consistent assignment, causing at least in theory extra work for finding satisfying assignments for the rest of the variables.
Given a (propositional) truth assignment $p$ and an SMT formula $f$ in CNF, if a literal $l$ appears only in clauses $c \in f$ that are satisfied by $p$, $l$ is called a ghost literal. Ghost literals have the property that they need not to be branched on to determine the satisfiability with respect to Prop. 2.2 above.
This issue studies ways of implementing ghost literal detection for opensmt and whether they would provide a performance boost for (in particular) satisfiable instances.
[1] Roberto Sebastiani: Lazy Satisability Modulo Theories. JSAT 3(3-4): 141-224 (2007)