A continuous local search SAT solver based on Fourier expansion for hybrid Boolean constraints.
FourierSAT is a continuous-optimization-based SAT/MaxSAT solver for hybrid Boolean constraints (CNF, XOR, cardinality constraints and not-all-equal) written in Python.
FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints
https://arxiv.org/abs/1912.01032
(AAAI-2020)
A comprehensive journal version:
Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions
https://akyrillidis.github.io/pubs/Journals/fourierSAT.pdf
(AI Journal-2021)
To achieve better performance, see GradSAT (https://github.com/vardigroup/GradSAT), an extension of FourierSAT. GradSAT is implemented in C++, where BDDs are used for accelerating gradient computations.
Also check our new work on equiping FourierSAT with GPUs and matrix multiplications with up to 100x accelerated gradient computation:
If you have questions or thoughts regarding the tool or this work, please contact zhiwei@rice.edu.
python with Scipy
python usage:
python FourierSAT/FourierSAT.py [DIMACS filepath] --options
*Optional parameters:
—timelimit: the time limit (in seconds) for this run. Default: 60
—tolerance: the number of clauses that a solution can violate. Default: 0
—cpus: the number of CPU cores available (the more, the better). Default: 8
—verbose: set it to 1 to output more information
For example:
FourierSAT sample.cnf --timelimit 10 --tolerance 1 --cpus 2 --verbose 1
FourierSAT accepts an extended DIMACS format which can handle CNF, XOR, cardinality constraints and Not-all-equal clauses. MaxSAT instances (.wcnf) and cardinality constraints encoded in pseudo-Boolean format (.opb) are also accepted.
CNF: “[literals] 0”
eg: clause x_1 or \neg x_2: "1 -2 0"
XOR: “x [literals] 0”
eg: clause x_1 xor \neg x_2: "x 1 -2 0"
Cardinality constraints: “d [k] [literals] 0”
k>0 means greater or equal
k<0 means less or equal
eg: x_1 + x_2 + x_4 + \neg x_5 >=2: "d 2 1 2 4 -5 0"
Alternatively, you can use the pseudo-Boolean encoding:
"1 x1 + 1 x2 + 1 x4 - 1 x5 >= 1"
if you want to include a global cardinality constraint (a constriant containing all variables and all the literals are positive), use a line “g [k]”. (Note: no ‘0’ at the end of the line!)
eg: x_1+x_2+x_3+x_4+x_5 <= 2: "g -2"
Not all equal: “n [literals] 0”
eg: NAE(x_1,x_2,\neg x_3): "n 1 2 -3 0"
-s "solved"/"not-solved in timelimit seconds"+[minimum number of violated clauses]-v [solutions]/[the assignment with minimum number of violated clauses found]-o [the cost of the best solution found so far (the number of violated constraints)] (Only for MaxSAT mode)