Results

DQBF Track QBFEVAL'18 With improved SAT-encodings and running standard SAT-solvers, we where able to compute the normalforms for all 334 instances in the DQBF track of QBFEVAL’18. All normalforms have been computed within a total time of 9000s. (We remark that finding an autarky is quick, and most of the time is spent on proving unsatisfiability.)

We found that there are exactly 4 instances with non-trivial A1-autarkies. 330 instances are E1+A1-lean (have no non-trivial E1- or A1-autarky). From the remaining 4 instances, all are E1-lean, one is A1-satisfiable, one is E1+A1-satisfiable, and the remaining two instances are not E1+A1-satisfiable, but allow A1-autarkies eliminating in both cases around 80% of variables and clauses (while adding E1 does not change this).

We have implemented the SAT tranlation into AutarkyFinder, that finds the A1, E1, A1 + E1 autarkies in the input (D)QBF. The C++ implementaion is around 1800 lines of code. The software allows the user to choose an autarky system for the reduction and different strictness levels of the input file besides other parameters like choice of encoding At Most One constraints.

We use n(F) for total number of variables, c(F) for number of clauses, a(F) for total number of universal variables and e(F) for total number of existential variables in the formula F.

Instance 1. bloem_eq1.dqdimacs A1_Autarky Satisfiable

 - Input formula:   
   n(F) = 9    
   c(F) = 16     
   a(F) = 1        
   e(F) = 8         
 - E1_Autarky (F): Lean (No reduction)  
 - A1_Autarky (F): Satisfiable   
     Autarky: (2 -> -1, 3 -> true, 4 -> true, 5 -> false,   
                6 -> false, 7 -> true, 8 -> true, 9 -> true)
 - E1 + A1_Autarky (F): Satisfiable  
     Autarky: Same as above   

Instance 2. tentrup17_ltl2dba_theta_environment_1.dqdimacs E1 + A1_Autarky Satisfiable

  - Input formula:  
    n(F) = 249  
    c(F) = 732  
    a(F) = 3     
    e(F) = 246     
  - E1_Autarky (F): Lean (No reduction)  
  - A1_Autarky (F): Non Trivial Autarky (Reduction but not SAT)  
      Remaining evars count: 17  
      Remaining clause count: 67  
  - E1 + A1_Autarky (F): Satisfiable   
      Autarky: Link   

Instance 3. bloem_ex1.dqdimacs Non-Trivial A1_Autarky

  - Input formula:  
    n(F) = 23  
    c(F) = 52  
    a(F) = 3          
    e(F) = 20         
  - E1_Autarky (F): Lean (No reduction)  
  - A1_Autarky (F): Non Trivial Autarky (Reduction but not SAT)  
      Remaining evars count: 6  
      Remaining clause count: 18  
  - E1 + A1_Autarky (F): Non trivial Autarky   
      Autarky: Same as above  

Instance 4. bloem_ex2.dqdimacs Non-Trivial A1_Autarky

 - Input formula:  
   n(F) = 60  
   c(F) = 139   
   a(F) = 10         
   e(F) = 50          
 - E1_Autarky (F): Lean (No reduction)  
 - A1_Autarky (F): Non Trivial Autarky (Reduction but not SAT)  
   Remaining evars count: 33  
   Remaining clause count: 99   
 - E1 + A1_Autarky (F): Non trivial Autarky   
   Autarky: Same as above