Computation And Applications Of Backbone Variables In SAT/SMT Formulas

The Boolean Satisfiability(SAT)problem has been widely applied to solve the related problems in the areas of program analysis,program verification,ma-chine learning and so on and so forth.Based on SAT theory,Satisfiability Modulo Theories(SMT)is able to solve the problems in the above areas more efficiently by combining Boolean constraints with Modulo constraints.Although there are already many applications of SAT/SMT Theories in practical problems,but the efficiency suffers numerous droppings when the practical problems are too com-plicated,which decreases the usability and scalability of SAT/SMT Theories in practice.To tackle the problems mentioned above,the author proposes new methods to compute the backbone variables of SAT/SMT formulas using returning messages from the SAT/SMT solvers.Based on the SAT/SMT structures and the returning messages from SAT/SMT formulas,the methods analyze the backbone variables in SAT/SMT formulas and design the computing framework for SAT/SMT backbone variables.The abilities of the proposed methods in finding every solutions of SAT formulas and finding adversarial examples in Deep Neural Network have been demonstrated by theoretical analysis and experimental comparison of the proposed methods.The main contributions are:(1)Studies and proposes a new framework to compute backbone variables for SAT Formulas.The framework analyzes the feature of back-bone variables in SAT formulas,and design and implement an efficient framework to compute backbone variables of SAT formulas based on their features.The framework finds backbone and non-backbone variables iteratively based on known backbone/non-backbone information.The approach is able to compute backbone variables for SAT formulas effi-ciently using SAT formulas structure information and known backbone variables information.Experiments show that the efficiency of the proposed approach is15%times faster than the existing approach.(2)Based on SAT backbone variables,studies and proposes a method to compute backbone variables for SMT formulas.For a SMT formula F,the method computes the corresponding SAT formula F_bof F,it then computes the some backbone variables of F_b.The method separate SMT formulas into small constraints and compute the Largest Available Interval for each backbone variables using optimizing configurations in the SMT solver.Comparing to the existing methods,the method is able to increase the efficiency of SMT solving by using less the solving of existing quantifier(?).Experiments show that the proposed approach is able reduce the number of SMT solving,including Quantifiers Solving and Boundaries Solving.The proposed approach is able to save 17%computing time for SMT backbone computation,and increase the efficiency of SMT backbone computing.(3)Based on SAT variables,studies and proposes an efficient method to compute all solutions for a given SAT formula.In order to find all solu-tions for a given formula F,it needs to convert the known solutions to constraints and add them to F to find new solutions.Comparing to the existing methods,the method is able to generate shorter constraints by using backbone variables of SAT formulas.By adding shorter constraints to the original formula,the scale of the new SAT formula has decreased and the SAT testing numbers have been decreased.By using backbone variable of SAT formulas,the method is able to accelerate the process of SAT testing.Experiments show that the proposed method is able to accelerate the com-putation of all solutions for a SAT formula,the method is 27%faster than the existing methods.(4)Based on SMT variables,studies and proposes an efficient tool to compute adversarial examples for Deep Neural Networks.The relia-bility of Deep Neural Network could be increased using adversarial examples,the proposed method uses backbone variables to compute adversarial examples.The method encodes Deep Neural Network into SMT formula F,computes the back-bone variables of F and the corresponding largest available assigning intervalr for each backbone variable.Given an input for the Deep Neural Network and a back-bone variable x in F,it uses the interval analysis to compute the largest available assigning interval r~?of x with the given input.If r is a subset of r~?,then there ex-ists an adversarial example for the given input.The method uses gradient descent to generate an adversarial example for the given input,the object function of the gradient descent used in the method is based on intervals r and r~?.Experiments show that the proposed method finds more adversarial examples than other existing methods.