Skip to content

Commit

Permalink
Update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
zbendefy authored Feb 8, 2018
1 parent ecd115d commit f07f56b
Showing 1 changed file with 9 additions and 3 deletions.
12 changes: 9 additions & 3 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,10 +1,16 @@
# opencl-satsolver

This is a Brute force sat solver, written in Java, and OpenCL (using the JOCL bindings). It basically parses the input expression, and tries every single variable configuration.
This is a simple Brute force sat solver, written in Java, and OpenCL (using the JOCL bindings). It basically parses the input expression, and tries every single variable configuration.

There is a test app included, that can be used to try the libs features.

##Features:
## Trying the library

Download the SatSolverTest.jar from the repository (or build it from the source), and run it from the command line:

java -jar SatSolverTest.jar

## Features:
* Supports expressions up to 62 boolean variables
* AND, OR, NEGATE operators
* Can evaluate expressions like: A & B | (C & !D)
Expand All @@ -16,5 +22,5 @@ Note that above 24-26 variables calculation times can be very-very long.

#### There are 2 methods implemented:
* The Single/simple solver will return a byte array where each byte represents a solution.
* The Multi solver will pack 8 results into a byte (each bit is represents 1 solution), to save on memory (and to allow more variables).
* The Multi solver will pack 8 results into a byte (each bit represents a solution), to save on memory (and to allow more variables).
For larger problems, the multi solver method is automatically selected.

0 comments on commit f07f56b

Please sign in to comment.