8 ms·

Kissat SAT Solver

111 points by veselin 6y ago

HPsquared 6y ago
To save the unwashed masses (myself included) any further internet searches, this relates to the Boolean satisfiability problem, which according to Wikipiedia [0] is: "the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable." I originally thought it was an AI to solve college placement tests, which would also have been cool but in a different way. [0]: https://en.wikipedia.org/wiki/Boolean_satisfiability_problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
- wiz21c 6y ago
  SAT solvers are really powerful machines. You can fit many problems in a Boolean formula and then ask the solver to work it out. Now, the solver is not always optimized for your task but sometimes it helps. Also, the exercise of turning a problem into a (usually huge) Boolean formula is interesting. For example, I solved the "find a longest path in a graph" with a SAT solver (TBH, I quickly replaced that with a specialized solver, but, well, that was fun !)
  - PaulHoule 6y ago
    SAT is the prototypical NP-complete problem.
    - agency 6y ago
      And indeed I think the reduction of NP problems to SAT is pretty intuitively understandable, at least at a hand-wavy level. If a decision problem is in NP, then given some candidate solution to the problem we can verify it in polynomial time. If you imagine a computer implementing this decision algorithm, and you squint your eyes, you can imagine it as a huge boolean satisfiability problem. The program takes some input (as bits aka boolean variables) and the program is run in the circuitry of the computer which at the bottom is effectively doing boolean algebra with logic gates and such. And so if you can solve SAT in polynomial time, then you can run it on this instance of SAT (the instantiation of the verifier for this NP problem) and find out if there's any input to that NP problem that satisfies it. Obviously there's a lot more work to make it formal.
    - maweki 6y ago
      While it is true, if you follow current research, most people in the field seem to be on a great hunt for hard SAT instances where no known heuristic really helps. As of yet this hunt has not been successful.
      - jlokier 6y ago
        A hard SAT problem: Let nonce be 32 boolean inputs, representing numbers from 0..2^32-1. Let other_bits and difficulty be a collection of constant boolean inputs, in the following expression. Let f(other_bits, nonce, diff) be the boolean logic circuit used in Bitcoin mining, for a recent candidate block. Roughly speaking, f combines nonce with other_bits to make a bit string, performs SHA-256 on the bit string, then SHA-256 on that, and then checks if the leading diff number of bits are zero. Folding in the constants, f reduces to a boolean logic circuit with 32 inputs and 1 output, g(nonce) = result. The SAT problem: Does there exist a value of nonce for which g(nonce) = 1? If you can solve this quickly, you just sped up Bitcoin mining by a factor 2^32 iterations, which is a lot. You can take this further as well. I don't know of any SAT solver heuristic which really helps with this.
        nightcracker 6y ago
        This SAT instance is huge, which makes it hard. But you haven't shown that it is a harder SAT instance than a random one of its size. It's all about the difficulty vs the size of the instance.
        jlokier 6y ago
        To the best of my knowledge, the example has no known heuristics for finding a solution that are significantly faster than brute force. That puts it in the hardest class of instances for its size (subject to available knowledge), because all instances can be solved by brute force.
        nightcracker 6y ago
        A SAT solver might very well have optimizations that make it end up running in 2^200 on average instead of what brute force would give. The problem is, since the instance is so large, we don't know what happens. No one has ever ran one to completion. So no, it's not in the hardest class of instances for its size. Its difficulty is unknown.
- jamestenglish 6y ago
  Thank you! I clicked all the links on the page and still had no idea what SAT or the SAT Competition was!
andrepd 6y ago
This is very exciting! It not only has much improved performance, but it's also clean code, easily extensible for embedding in other applications (I do such a thing myself). Sadly I can't use it yet due to lack of incremental solving.
thechao 6y ago
If anyone else is wondering how the hell to use this thing... the main API is here: https://github.com/arminbiere/kissat/blob/master/src/kissat.h In particular all you need to add clauses is this single API entry point: void kissat_add (kissat * solver, int lit); The solver consists of the conjunction of disjunctions (I hope I have that correct — maybe the other way around? I can never remember). Variables are assumed to be any non-zero integer: kissat_add(s, [N != 0]); You create a clause by repeatedly calling kissat_add; the clause is terminated by a 0. For instance if {shirt=1, tie=2}, then "!shirt or tie" is: kissat_add(s, -1); kissat_add(s, 2); kissat_add(s, 0); Once the solver is run, if there's a solution, you get the solution using `kissat_val`: kissat_val(s, 1); kissat_val(s, 2); I hope.
- throwawaygh 6y ago
  It supports the DIMACS input format [1], which you can parse using the kissat_parse_dimacs function [2]. DIMACS is a pretty terrible format, but at least you don't have to build the clauses up yourself using kissat_add. [1] http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/SATLINK____DIMACS http://www.cs.utexas.edu/users/moore/acl2/manuals/current/ma... [2] https://github.com/arminbiere/kissat/blob/master/src/parse.h https://github.com/arminbiere/kissat/blob/master/src/parse.h
- amelius 6y ago
  How do you interrupt the computation, e.g. when it takes too long?
  - mgraczyk 6y ago
    You could always fork the process and send SIGKILL to the child after a timeout.
    - jwilk 6y ago
      No need to fork; you could install timer using alarm(), setitimer(), or timer_create() and friends.
gallerdude 6y ago
Question: in college, I was lead to believe that a polynomial time SAT solver would be a huge breakthrough in many fields. Why is that the case? I know 3SAT is a reduction to NP problems, but besides that I feel like it wouldn't be particularly useful on its own.
- IanCal 6y ago
  I think that's it. If you can reduce your NP problems to 3SAT and 3SAT is in P then all P=NP.
- teraflop 6y ago
  If 3SAT is solvable in polynomial time, then P=NP. Which means that any problem that can be solved by brute-forcing an exponential number of possibilities (and doing a polynomial amount of checking for each) can also be solved with an asymptotically much smaller (polynomial) amount of work. This includes anything from complicated optimization problems, to theorem proving, to inverting cryptographic hash functions, to any other NP algorithm that hasn't been thought up yet. Whether this would have any practical use would depend on the polynomial exponents and constant factors, of course. But even in a theoretical sense it would be very, very surprising to a lot of people if it were true.
  - schoen 6y ago
    Donald Knuth apparently believes, in a very unusual view for a computer scientist, that P=NP but that the best algorithm has such bad exponents and factors that it won't have relevance for our computational practices -- if we're even able to discover it. https://www.informit.com/articles/article.aspx?p=2213858&ranMID=24808 https://www.informit.com/articles/article.aspx?p=2213858&ran...
- X6S1x6Okd1st 6y ago
  It'd be a breakthrough, but only for problems big enough that the cost (polynomial & constant) of translating to and from SAT would be worth it for the problem at hand. Also P=NP would be a very big deal.
7373737373 6y ago
I wonder how big of an economic impact such improved algorithms have. Must be in the billions of dollars in the long run...
hinkley 6y ago
Are there any software development problems we should be solving with SAT solvers instead of using heuristics?
- klyrs 6y ago
  Various sorts of scheduling problems come to mind... for example compilers can make good use of a fast sat solver; but typically you want a failover heuristic so you won't spend forever on large or unsolvable problems
- dragontamer 6y ago
  Any problem that works. IIRC: SAT Solvers regularly solve 30,000+ nodes of traveling salesman problem in just seconds (Or something along that magnitude. I forget exactly...). Yeah, its NP complete, but that doesn't mean its worthless. It will take some experimentation to figure out if your problem is within the "feasible" category of SAT solving. I don't think there's any method aside from "try it, and if it works, be happy. If not, be sad". If we knew which problems were easily solved with SAT-solvers, we probably would be well on our way to proving N == NP ?? So just guess and check. -------------- Honestly, people may forget that brute-force solvers can be incredibly useful. When I was playing with a hash-algorithm I was inventing (just for fun on the side...) I searched the entire 32-bit space for the best integer that best mixed-up the bits from input to output. The brute-force solver took only seconds to try every 32-bit number. We can brute-force a surprising number of "intractable" problems from our college years. Yeah, its inefficient, but who cares if its solved in seconds or minutes? There's also that a^3 + b^3 == c^3 problem that was solved in a few weeks by brute forcing every number (or something like that).
  - jwilk 6y ago
    > There's also that a^3 + b^3 == c^3 problem that was solved in a few weeks by brute forcing every number (or something like that). Huh?
    - analognoise 6y ago
      There are only so many numbers, we simply tried them all. It took a really large computer. /s
ipnon 6y ago
Computational logic seems to be a more popular research subject in Europe than in the United States.
throwmemoney 6y ago
SAT Solvers are used in software that is used in creating the very complex Silicon Chips. Known as Formal in the semiconductor design industry.
schoen 6y ago
For obscure reasons I know that this is the Finnish word for 'cats', and I wondered if there was any connection there. Apparently the answer is yes https://github.com/arminbiere/kissat https://github.com/arminbiere/kissat or at least the developers have already noticed this coincidence for themselves.
psandersen 6y ago
I've been looking to get my feet wet with SAT and/or SMT solvers; can anyone recommend any short courses that I could start with to get a practical feel where where & how to use them? Python would be preferred. Maybe this https://www.coursera.org/learn/automated-reasoning-sat https://www.coursera.org/learn/automated-reasoning-sat would be a good start? Ideally I would like to be able to take predicted outputs from ML plus business requirements to solve allocation problems; and more pie in the sky I would like to know enough to get inspiration for how to link a neural network with a sat solver, such as perhaps replacing or augmenting beam search in sequence decoding tasks.

111 points by veselin 6y ago

To save the unwashed masses (myself included) any further internet searches, this relates to the Boolean satisfiability problem, which according to Wikipiedia [0] is: "the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable." I originally thought it was an AI to solve college placement tests, which would also have been cool but in a different way. [0]: https://en.wikipedia.org/wiki/Boolean_satisfiability_problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem

wiz21c 6y ago
SAT solvers are really powerful machines. You can fit many problems in a Boolean formula and then ask the solver to work it out. Now, the solver is not always optimized for your task but sometimes it helps. Also, the exercise of turning a problem into a (usually huge) Boolean formula is interesting. For example, I solved the "find a longest path in a graph" with a SAT solver (TBH, I quickly replaced that with a specialized solver, but, well, that was fun !)
- PaulHoule 6y ago
  SAT is the prototypical NP-complete problem.
  - agency 6y ago
    And indeed I think the reduction of NP problems to SAT is pretty intuitively understandable, at least at a hand-wavy level. If a decision problem is in NP, then given some candidate solution to the problem we can verify it in polynomial time. If you imagine a computer implementing this decision algorithm, and you squint your eyes, you can imagine it as a huge boolean satisfiability problem. The program takes some input (as bits aka boolean variables) and the program is run in the circuitry of the computer which at the bottom is effectively doing boolean algebra with logic gates and such. And so if you can solve SAT in polynomial time, then you can run it on this instance of SAT (the instantiation of the verifier for this NP problem) and find out if there's any input to that NP problem that satisfies it. Obviously there's a lot more work to make it formal.
  - maweki 6y ago
    While it is true, if you follow current research, most people in the field seem to be on a great hunt for hard SAT instances where no known heuristic really helps. As of yet this hunt has not been successful.
    - jlokier 6y ago
      A hard SAT problem: Let nonce be 32 boolean inputs, representing numbers from 0..2^32-1. Let other_bits and difficulty be a collection of constant boolean inputs, in the following expression. Let f(other_bits, nonce, diff) be the boolean logic circuit used in Bitcoin mining, for a recent candidate block. Roughly speaking, f combines nonce with other_bits to make a bit string, performs SHA-256 on the bit string, then SHA-256 on that, and then checks if the leading diff number of bits are zero. Folding in the constants, f reduces to a boolean logic circuit with 32 inputs and 1 output, g(nonce) = result. The SAT problem: Does there exist a value of nonce for which g(nonce) = 1? If you can solve this quickly, you just sped up Bitcoin mining by a factor 2^32 iterations, which is a lot. You can take this further as well. I don't know of any SAT solver heuristic which really helps with this.
      - nightcracker 6y ago
        This SAT instance is huge, which makes it hard. But you haven't shown that it is a harder SAT instance than a random one of its size. It's all about the difficulty vs the size of the instance.
        jlokier 6y ago
        To the best of my knowledge, the example has no known heuristics for finding a solution that are significantly faster than brute force. That puts it in the hardest class of instances for its size (subject to available knowledge), because all instances can be solved by brute force.
        nightcracker 6y ago
        A SAT solver might very well have optimizations that make it end up running in 2^200 on average instead of what brute force would give. The problem is, since the instance is so large, we don't know what happens. No one has ever ran one to completion. So no, it's not in the hardest class of instances for its size. Its difficulty is unknown.
jamestenglish 6y ago
Thank you! I clicked all the links on the page and still had no idea what SAT or the SAT Competition was!

andrepd 6y ago

This is very exciting! It not only has much improved performance, but it's also clean code, easily extensible for embedding in other applications (I do such a thing myself). Sadly I can't use it yet due to lack of incremental solving.

thechao 6y ago

If anyone else is wondering how the hell to use this thing... the main API is here: https://github.com/arminbiere/kissat/blob/master/src/kissat.h In particular all you need to add clauses is this single API entry point: void kissat_add (kissat * solver, int lit); The solver consists of the conjunction of disjunctions (I hope I have that correct — maybe the other way around? I can never remember). Variables are assumed to be any non-zero integer: kissat_add(s, [N != 0]); You create a clause by repeatedly calling kissat_add; the clause is terminated by a 0. For instance if {shirt=1, tie=2}, then "!shirt or tie" is: kissat_add(s, -1); kissat_add(s, 2); kissat_add(s, 0); Once the solver is run, if there's a solution, you get the solution using `kissat_val`: kissat_val(s, 1); kissat_val(s, 2); I hope.

throwawaygh 6y ago
It supports the DIMACS input format [1], which you can parse using the kissat_parse_dimacs function [2]. DIMACS is a pretty terrible format, but at least you don't have to build the clauses up yourself using kissat_add. [1] http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/SATLINK____DIMACS http://www.cs.utexas.edu/users/moore/acl2/manuals/current/ma... [2] https://github.com/arminbiere/kissat/blob/master/src/parse.h https://github.com/arminbiere/kissat/blob/master/src/parse.h
amelius 6y ago
How do you interrupt the computation, e.g. when it takes too long?
- mgraczyk 6y ago
  You could always fork the process and send SIGKILL to the child after a timeout.
  - jwilk 6y ago
    No need to fork; you could install timer using alarm(), setitimer(), or timer_create() and friends.

gallerdude 6y ago

Question: in college, I was lead to believe that a polynomial time SAT solver would be a huge breakthrough in many fields. Why is that the case? I know 3SAT is a reduction to NP problems, but besides that I feel like it wouldn't be particularly useful on its own.

IanCal 6y ago
I think that's it. If you can reduce your NP problems to 3SAT and 3SAT is in P then all P=NP.
teraflop 6y ago
If 3SAT is solvable in polynomial time, then P=NP. Which means that any problem that can be solved by brute-forcing an exponential number of possibilities (and doing a polynomial amount of checking for each) can also be solved with an asymptotically much smaller (polynomial) amount of work. This includes anything from complicated optimization problems, to theorem proving, to inverting cryptographic hash functions, to any other NP algorithm that hasn't been thought up yet. Whether this would have any practical use would depend on the polynomial exponents and constant factors, of course. But even in a theoretical sense it would be very, very surprising to a lot of people if it were true.
- schoen 6y ago
  Donald Knuth apparently believes, in a very unusual view for a computer scientist, that P=NP but that the best algorithm has such bad exponents and factors that it won't have relevance for our computational practices -- if we're even able to discover it. https://www.informit.com/articles/article.aspx?p=2213858&ranMID=24808 https://www.informit.com/articles/article.aspx?p=2213858&ran...
X6S1x6Okd1st 6y ago
It'd be a breakthrough, but only for problems big enough that the cost (polynomial & constant) of translating to and from SAT would be worth it for the problem at hand. Also P=NP would be a very big deal.

7373737373 6y ago

I wonder how big of an economic impact such improved algorithms have. Must be in the billions of dollars in the long run...

hinkley 6y ago

Are there any software development problems we should be solving with SAT solvers instead of using heuristics?

klyrs 6y ago
Various sorts of scheduling problems come to mind... for example compilers can make good use of a fast sat solver; but typically you want a failover heuristic so you won't spend forever on large or unsolvable problems
dragontamer 6y ago
Any problem that works. IIRC: SAT Solvers regularly solve 30,000+ nodes of traveling salesman problem in just seconds (Or something along that magnitude. I forget exactly...). Yeah, its NP complete, but that doesn't mean its worthless. It will take some experimentation to figure out if your problem is within the "feasible" category of SAT solving. I don't think there's any method aside from "try it, and if it works, be happy. If not, be sad". If we knew which problems were easily solved with SAT-solvers, we probably would be well on our way to proving N == NP ?? So just guess and check. -------------- Honestly, people may forget that brute-force solvers can be incredibly useful. When I was playing with a hash-algorithm I was inventing (just for fun on the side...) I searched the entire 32-bit space for the best integer that best mixed-up the bits from input to output. The brute-force solver took only seconds to try every 32-bit number. We can brute-force a surprising number of "intractable" problems from our college years. Yeah, its inefficient, but who cares if its solved in seconds or minutes? There's also that a^3 + b^3 == c^3 problem that was solved in a few weeks by brute forcing every number (or something like that).
- jwilk 6y ago
  > There's also that a^3 + b^3 == c^3 problem that was solved in a few weeks by brute forcing every number (or something like that). Huh?
  - analognoise 6y ago
    There are only so many numbers, we simply tried them all. It took a really large computer. /s

ipnon 6y ago

Computational logic seems to be a more popular research subject in Europe than in the United States.

throwmemoney 6y ago

SAT Solvers are used in software that is used in creating the very complex Silicon Chips. Known as Formal in the semiconductor design industry.

schoen 6y ago

For obscure reasons I know that this is the Finnish word for 'cats', and I wondered if there was any connection there. Apparently the answer is yes https://github.com/arminbiere/kissat https://github.com/arminbiere/kissat or at least the developers have already noticed this coincidence for themselves.

psandersen 6y ago

I've been looking to get my feet wet with SAT and/or SMT solvers; can anyone recommend any short courses that I could start with to get a practical feel where where & how to use them? Python would be preferred. Maybe this https://www.coursera.org/learn/automated-reasoning-sat https://www.coursera.org/learn/automated-reasoning-sat would be a good start? Ideally I would like to be able to take predicted outputs from ML plus business requirements to solve allocation problems; and more pie in the sky I would like to know enough to get inspiration for how to link a neural network with a sat solver, such as perhaps replacing or augmenting beam search in sequence decoding tasks.