How can you possibly solve a mission-critical problem with millions of variables—when the worst-case computational complexity of every known algorithm for that problem is exponential in the number of variables?
SAT (Satisfiability) solvers have seen dramatic orders-of-magnitude performance gains for many problems through algorithmic improvements over the last couple of decades or so. The SAT problem—finding an assignment of Boolean variables that makes a given Boolean expression true—represents the archetypal NP-complete problem and in the general case is intractable.
However, for many practical problems, solutions can be found very efficiently by use of modern methods. This “killer app” of computer science, as described by Donald Knuth, has applications to many areas, including software verification, electronic design automation, artificial intelligence, bioinformatics, and planning and scheduling.
Its uses are surprising and diverse, from running billion dollar auctions to solving graph coloring problems to computing solutions to Sudoku puzzles. As an example, I’ve included a toy code below that uses SMT, a relative of SAT, to find the English language suffix rule for regular past tense verbs (“-ed”) from data.
When used as a machine learning method, SAT solvers are quite different from other methods such as neural networks. SAT solvers can for some problems have long or unpredictable runtimes (though MAXSAT can sometimes relax this restriction), whereas neural networks have essentially fixed inference cost (though looping agent-based models do not).
On the other hand, answers from SAT solvers are always guaranteed correct, and the process is interpretable; this is currently not so for neural network-based large language models.
To understand better how to think about this difference in method capabilities, we can take a lesson from the computational science community. There, it is common to have a well-stocked computational toolbox of both slow, accurate methods and fast, approximate methods.
In computational chemistry, ab initio methods can give highly accurate results by solving Schrödinger’s equation directly, but only scale to limited numbers of atoms. Molecular dynamics (MD), however, relies more on approximations, but scales efficiently to many more atoms. Both are useful in different contexts. In fact, the two methodologies can cross-pollenate, for example when ab initio calculations are used to devise force fields for MD simulations.
A lesson to take from this is, it is paramount to find the best tool for the given problem, using any and all means at one’s disposal.
The following are some of my favorite general references on SAT solvers:
- Donald Knuth, The Art Of Computer Programming: Volume 4 Fascicle 6, Satisfiability. A coherent introduction to the methods, accessible to the mathematically inclined.
- Marijn J.H. Heule, Advanced Topics in Logic: Automated Reasoning and Satisfiability. Slides from an advanced class by one of the world experts.
- A. Biere, H. van Maaren, M. Heule, eds, Handbook of Satisfiability. An in-depth tome on state of the art, arranged topically.
- Daniel Kroening and Ofer Strichman, Decision Procedures: An Algorithmic Point of View. An accessible book on an important class of extensions to SAT: satisfiability modulo theories (SMT), which make SAT-type methods applicable to a much wider range of problems.
- Documentation for Z3, an innovative open-source solver for solving SAT, SMT, MAXSAT and combinatorial optimization problems.
- Simons Institute workshops here, here, here. here and here covering a great range of topics and state of the art research.
It would seem that unless P = NP, commonly suspected to be false, the solution of these kinds of problems for any possible input is hopelessly beyond reach of even the world’s fastest computers. Thankfully, many of the problems we care about have an internal structure that makes them much more solvable (and likewise for neural networks). Continued improvement of SAT/SMT methods, in theory and implementation, will greatly benefit the effective solution of these problems.
A toy example: find the English past tense suffix rule using Z3
import csv import z3 def char2int(c): return ord(c) - ord('a') def int2char(i): return chr(i + ord('a')) # Access the language data from the file. with open('eng_cols.txt', newline='') as csvfile: reader = csv.reader(csvfile, delimiter='\t') table = [row for row in reader] nrow, ncol = len(table), len(table[0]) # Identify which columns of input table have stem and targeted word form. stem_col, form_col = 0, 1 # Calculate word lengths. nstem = [len(table[i][stem_col]) for i in range(nrow)] nform = [len(table[i][form_col]) for i in range(nrow)] # Length of suffix being sought. ns = 2 # Initialize optimizer. solver = z3.Optimize() # Define variables to identify the characters of suffix; add constraints. var_suf = [z3.Int(f'var_suf_{i}') for i in range(ns)] for i in range(ns): solver.add(z3.And(var_suf[i] >= 0, var_suf[i] < 26)) # Define variables to indicate whether the given word matches the rule. var_m = [z3.Bool(f'var_m_{i}') for i in range(nrow)] # Loop over words. for i in range(nrow): # Constraint on number of characters. constraints = [nform[i] == nstem[i] + ns] # Constraint that the form contains the stem. for j in range(nstem[i]): constraints.append( table[i][stem_col][j] == table[i][form_col][j] if j < nform[i] else False) # Constraint that the end of the word form matches the suffix. for j in range(ns): constraints.append( char2int(table[i][form_col][nform[i]-1-j]) == var_suf[j] if j < nform[i] else False) # var_m[i] is the "and" of all these constraints. solver.add(var_m[i] == z3.And(constraints)) # Seek suffix that maximizes number of matches. count = z3.Sum([z3.If(var_m[i], 1, 0) for i in range(nrow)]) solver.maximize(count) # Run solver, output results. if solver.check() == z3.sat: model = solver.model() suf = [model[var_suf[i]] for i in range(ns)] print('Suffix identified: ' + ''.join(list([int2char(suf[i].as_long()) for i in range(ns)]))[::-1]) print('Number of matches: ' + str(model.evaluate(count)) + ' out of ' + str(nrow) + '.') var_m_values = [model[var_m[i]] for i in range(nrow)] print('Matches:') for i in range(nrow): if var_m_values[i]: print(table[i][stem_col], table[i][form_col])
Love this stuff! Thanks for this post….
Amazon Science has a strong team here. This post (below) offers context, pretty pictures, competition members and results, and some future prognostications.
https://www.amazon.science/blog/automated-reasonings-scientific-frontiers
Why these kind of tools & techniques are not every bit as ‘popular’ as Large Hallucination and Crowdspeak algorithms is mildly mystifying to me…
Nice article, thanks for sharing. Many problems it would seem are just too complicated structurally and will make SAT solvers “hang” without prior indication. That being said, the range of potential applications of these solvers seems very underexplored.
Is the training data “english_cols.txt” available online, somewhere?
Hi Tom, here is some sample data. Each line should have two tab-separated words, you may need to fix, as it may get mangled by the posting process —
ask asked
burn burned
walk walked
consider considered
count counted
chase chased
confuse confused
create created
dance danced
deceive deceived
study studied
copy copied
crucify crucified
cry cried
empty emptied
annoy annoyed
enjoy enjoyed
commit committed
control controlled
dip dipped
drop dropped
grab grabbed
plan planned
regret regretted
trip tripped
wrap wrapped
cover covered
deliver delivered
enter entered
gather gathered
honor honored
hover hovered
offer offered
remember remembered
frighten frightened
happen happened
listen listened
open opened
mix mixed
do did
go went
cut cut
fall fell
feed fed
fight fought
fly flew
give gave
make made
see saw
take took
Thank you, Wayne! That worked.
Thanks for sharing this.