SatEX: Satisfiability modulo convEX optimization solver 1. Introduction ----------------- This Python package contains the implementation of the algorithms described in the paper "SMC: Satisfiability Modulo Convex Optimization", Shoukry et al, HSCC 2017. This file describes the contents of the package, and provides instructions regarding its use. This package is used to generate all the figures documented in Section 6 (entitled “Results”) in the paper, i.e., Figure 3, Figure 4, Figure 5, and Figure 6. 2. Installation ----------------- The tool was written for Python 2.7.10. Earlier versions may be sufficient, but not tested. In addition to Python 2.7.10, the solver requires the following: - CPLEX Optimizer (https://www-01.ibm.com/software/commerce/optimization/cplex-optimizer/), an optimization package for LP, QP, QCP, MIP, provided for free for academic use via the IBM Academic Initiative. - CPLEX Python Interface. To install the Python API for CPLEX, please follow the instructions at the following URL: http://www.ibm.com/support/knowledgecenter/SSSA5P_12.5.0/ilog.odms.cplex.help/CPLEX/GettingStarted/topics/set_up/Python_setup.html 3. Running the experiments described in the paper --------------------------------------------------- The package includes five experiments. The files related to each experiment can be found in different subfolders (one for each experiment). To run any example, change the directory to one of the subfolders, and then run the python file inside. Details about each experiment and the expected results can be found below. HSCC16Paper90.pdf is a copy of the paper. Each benchmark writes the execution times of different solvers or for different configurations in separate .txt files (one file per each solver and configuration). The expected output files are zipped and provided in each subfolder as a reference. All the figures in the paper are generated using these text files. The reference output files are generated using a MacBook Pro laptop with the following specifications: - Processor: 2.5 GHz Intel Core i7 - Memory: 16 GB 1600 MHz DDR3 Different runs for the same test case can lead to slightly different execution times. 4. Description of the Experiments --------------------------------------------------- ———————————————————————————————————————————————————— Subfolder “01 Scalability Boolean” ———————————————————————————————————————————————————— The purpose of this experiment is to test the scalability of the following solvers: 1) SatEX - proposed in our paper 2) CPLEX - a state-of-the-art mixed integer programming suite 3) Z3 - as state-of-the-art SMT solver on logic formulas with increasing numbers of Boolean constraints. - 003-23-80.cnf: Includes a set of Boolean constraints encoded in CNF format. This file contains more than 130,000 Boolean constraints. - ScalabilityBoolean_100rVars.py: Reads the Boolean constraints in the “003-23-80.cnf” file. For each test case, we select the first k Boolean constraints from the file, where k takes a value in the following list: Test case list = { 1000, 5000, 10000, 15000, 20000, 25000, 30000, 35000, 40000, 45000, 50000, 55000, 60000, 65000, 70000, 75000, 80000, 85000, 90000, 95000, 100000, 105000, 110000, 115000, 120000, 125000, 130000}. The script also generates 50 random linear constraints, chooses a set of Boolean variables from the .cnf file and associates one linear constraint to each of these Boolean variables to construct an implication clause as described in the paper. The following solvers are then used to find satisfying assignments for both the Boolean and real variables: - SatEX - CPLEX (running on 1 core) - CPLEX (running on 4 cores) - Z3 Run > python ScalabilityBoolean_100rVars.py Outputs: - scalbality_100_SMC_results.txt: contains the execution times for the SatEX solver - scalbality_100_MILP1_results.txt: contains the execution times for the CPLEX solver (running on 1 core) - scalbality_100_MILP4_results.txt: contains the execution times for the CPLEX solver (running on 4 cores) - scalbality_100_Z3_results.txt: contains the execution times for Z3 SMT solver The execution times reported in these files are used to generate Figure 3(a) ———————————————————————————————————————————————————— Subfolder “02 Scalability Real” ———————————————————————————————————————————————————— The purpose of this experiment is to test the scalability of the following solvers: 1) SatEX - proposed in our paper 2) CPLEX - a state-of-the-art mixed integer programming suite 3) Z3 - as state-of-the-art SMT solver on logic formulas with an increasing number of real variables and constraints. - 003-23-80.cnf: Includes a set of Boolean constraints encoded in CNF format. This file contains more than 130,000 Boolean constraints. - ScalabilityReal.py: Reads the Boolean constraints in the “003-23-80.cnf” file and chooses the first 7000 constraint. Next it generates a set of k/2 random linear constraints, each with a number of real variables equal to k, where k takes a value in the following list: Test cases = {500, 1000, 1500, 2000, 2500, 3000, 3500, 4000, 4500, 5000}. Then, the script chooses a set of Boolean variables and associates one linear constraint to each of these Boolean variables via implication clauses. The following solvers are then used to find satisfying assignments for both the Boolean and the real variables: - SatEX - CPLEX (running on 1 core) - CPLEX (running on 4 cores) - Z3 Run > python ScalabilityReal.py Output: - scalbality_reals_SMC_results.txt: contains the execution times for the SatEX solver - scalbality_reals_MILP1_results.txt: contains the execution times for the CPLEX solver (running on 1 core) - scalbality_reals_MILP4_results.txt: contains the execution times for the CPLEX solver (running on 4 cores) - scalbality_reals_Z3_results.txt: contains the execution times for Z3 SMT solver The timeout period is set to 100 seconds Execution times reported in these files are used to generate Figure 3(b) ———————————————————————————————————————————————————— Subfolder “03 Scalability UNSAT” ———————————————————————————————————————————————————— The purpose of this experiment is to test the scalability of the following solvers: 1) SatEX - proposed in our paper 2) CPLEX - a state-of-the-art mixed integer programming suite 3) Z3 - as state-of-the-art SMT solver on SMC formulas such that the Boolean component is known to be unsatisfiable. - uufxxx-xxx.cnf: these files contains a set of Boolean constraints which are verified to be unsatisfiable. - ScalabilityUNSAT.py: Reads the Boolean constraints in the uufxxx-xxx.cnf files, generates 25 random linear constraints, chooses a set of Boolean variables and associate a linear constraint to each these Boolean variables via implication clauses. The following solvers are then used to find satisfying assignments for both the Boolean and the real variables: - SatEX - CPLEX (running on 1 core) - CPLEX (running on 4 cores) - Z3 Run > ScalabilityUNSAT.py Output: - scalbality_unsat_SMC_results.txt: contains the execution times for the SatEX solver - scalbality_unsat_MILP1_results.txt: contains the execution times for the CPLEX solver (running on 1 core) - scalbality_unsat_MILP4_results.txt: contains the execution times for the CPLEX solver (running on 4 cores) - scalbality_unsat_Z3_results.txt: contains the execution time for the Z3 solver Execution times reported in these files are used to generate Figure 4 ———————————————————————————————————————————————————— Subfolder “04 Secure State Estimation” ———————————————————————————————————————————————————— The purpose of this experiment is to test the scalability of the following solvers: 1) SatEX - proposed in our paper 2) CPLEX - a state-of-the-art mixed integer programming suite 3) Z3 - as state-of-the-art SMT solver when used to solve the secure state estimation problem (defined in Section 6.2). - ScalabilitySecureStateEstimation.py: Generates random instances of the secure state estimation. For all the test cases, the state dimension is fixed to 5, the maximum number of sensors being under attack is set to 5. The experiments consist in increasing the number of sensors (hence the number of Boolean variables and convex constraints). Test cases: 25, 50, 75, 100, 125, 150, 175, 200 The following solvers are then used to find satisfying assignments for both the Boolean and real variables: - SatEX (using SSF-based UNSAT certificates) - SatEX (using IIS-based UNSAT certificates) - CPLEX (running on 1 core) - CPLEX (running on 4 cores) - Z3 Outputs: - scalbality_SSE_SMC_SSF_results.txt: contains the execution times for the SatEX solver (using SSF-based certificates) - scalbality_SSE_SMC_IIS_results: contains the execution times for the SatEX solver (using IIS-based certificates) - scalbality_SSE_MILP2_results.txt: contains the execution times for the CPLEX solver (running on 2 cores) - scalbality_SSE_MILP4_results.txt: contains the execution times for the CPLEX solver (running on 4 cores) - scalbality_SSE_Z3_results.txt: contains the execution times for the Z3 solver The timeout period is set to 600 seconds Execution times reported in these files are used to generate Figure 5 ———————————————————————————————————————————————————— Subfolder “05 Motion Planning” ———————————————————————————————————————————————————— The purpose of this experiment is to test the scalability of the following solvers: 1) SatEX - proposed in our paper 2) CPLEX - a state-of-the-art mixed integer programming suite when used to solve the motion planning problem (defined in Section 6.3). - ScalabilityLTLMotionPlanning.py: Generates different instances of the motion planning problem. The following solvers are then used to find satisfying assignments for both Boolean and real variables: - SatEX (using PREFIX-based UNSAT certificates) - SatEX (using IIS-based UNSAT certificates) - CPLEX (running on 1 core) Outputs: - scalbality_motionplanning_PREFIX_results.txt: contains the execution times for the SatEX solver (using SSF-based certificates) - scalbality_motionplanning_IIS_results.txt: contains the execution times for the SatEX solver (using IIS-based certificates) - scalbality_motionplanning_MILP_results.txt: contains the execution times for the CPLEX solver (running on 2 cores) Execution times reported in these files are used to generate Figure 6