Test_3sat_solvers.py

gistfile1.txt

import random
import time
import itertools
import numpy as np
import os
import numpy as np
import json
from tqdm import tqdm
from pysat.solvers import Glucose42, Minicard, Lingeling, Cadical153, Minisat22,MapleChrono, Mergesat3

from easysat.generators import KSAT_Generator
from easysat.solvers import BruteForce, DPLL

################
%%time

ksg = KSAT_Generator()


brute_force_times = []
dpll_times = []
glucose_times = []
cadical_times = []
ms_times = []
lg_times = []
maple_times = []

MAX_LITERALS = 20 # Total number of literals to check up to
literals = list(range(3,MAX_LITERALS))
trials = 50 # Number of trials for each literal


hardest_problems = {}

for num_literals in tqdm(literals, total = len(literals)):
    
    _brute_force_times = []
    _dpll_times = []
    _glucose_times = []
    _cadical_times = []
    _ms_times = []
    _lg_times = []
    _maple_times = []

    # Sample trials from the critical region
    for num_conjuncts in [np.random.randint(num_literals*4,num_literals*5) for i in range(trials)]:

        # Sample a random 3SAT clause
        sample = ksg.random_kcnf(n_literals = num_literals, n_conjuncts=num_conjuncts)
        
        # Initialize solver
        g = Glucose42()
        c = Minicard()
        ms = Lingeling()
        maple = Mergesat3()
        dpll = DPLL()
        bfs = BruteForce()
        
        # Covert clauses to proper format
        sample_cnf = ksg.kcnf_to_cnf(sample)
        
        g.append_formula(sample_cnf)
        c.append_formula(sample_cnf)
        ms.append_formula(sample_cnf)
        maple.append_formula(sample_cnf)
        dpll.append_formula(sample_cnf)
        bfs.append_formula(sample_cnf)

        try:
            ## Time BFS
            if num_literals <= 15:
                start = time.time()
                _,answer, assigns = bfs.solve()
                runtime = time.time() - start
                _brute_force_times.append(assigns)
                

            if num_literals <= 20:
                ## Time DPLL
                start = time.time()
                #_,answer,assigns = dpll.solve()
                runtime = time.time() - start
                _dpll_times.append(assigns)
                #_dpll_times.append(runtime)
            
            
            ## Time Glucose
            start = time.time()
            result = g.solve()
            runtime = time.time() - start
            _glucose_times.append(g.accum_stats()['propagations'])
            #_glucose_times.append(runtime)
            
            props = g.accum_stats()['propagations']
            if num_literals not in hardest_problems.keys():
                hardest_problems[num_literals] = (sample_cnf, props, result, answer)
            elif hardest_problems[num_literals][1] < props:
                hardest_problems[num_literals] = (sample_cnf, props, result, answer)
                
    
            ## Time Cadical
            start = time.time()
            c.solve()
            runtime = time.time() - start
            _cadical_times.append(c.accum_stats()['propagations'])
            #_cadical_times.append(runtime)
            
            ## Time Minisat
            start = time.time()
            ms.solve()
            runtime = time.time() - start
            _ms_times.append(ms.accum_stats()['propagations'])
            #_ms_times.append(runtime)
            
            ## Time Maple
            start = time.time()
            maple.solve()
            runtime = time.time() - start
            _maple_times.append(maple.accum_stats()['propagations'])
            #_maple_times.append(runtime)
        
            if num_literals <= 15:
                brute_force_times.append(np.max(_brute_force_times))
            if num_literals <= 20:
                dpll_times.append(np.max(_dpll_times))
        except Exception as e:
            print(e)
            pdb.set_trace()

    
    glucose_times.append(np.max(_glucose_times))
    cadical_times.append(np.max(_cadical_times))
    ms_times.append(np.max(_ms_times))
    maple_times.append(np.max(_maple_times))
    
################
plt.style.use('tableau-colorblind10')
fig, axes = plt.subplots(figsize = (20,10))

axes.plot(literals[:len(brute_force_times)], brute_force_times, label = "Brute Force Search")
axes.plot(literals[:len(dpll_times)], dpll_times, label = "DPLL")
axes.plot(literals[:len(glucose_times)], glucose_times, label = "Glucose 3.4")
axes.plot(literals, cadical_times, label = "Minicard")
axes.plot(literals, ms_times, label = "Lingeling")
axes.plot(literals, maple_times, label = "Mergesat3")
axes.plot(literals, [1.15**n for n in literals], linestyle = '--', label = "F(x) = (1.15)^x")
axes.set_ylim(0, 2000)
axes.set_xlabel("# of Literals")
axes.set_ylabel("Worst Case # of Propagations [out of n=50 runs per # of literals]")
axes.set_xticks(literals)
plt.suptitle("Performance of Modern Solvers on Random 3-SAT Formulas", fontsize = 16, y= 0.92)
#plt.title("Worst Case out of n=100 runs per # of literals", fontsize = 10, y = 0.99)


axes.legend()