FourierSAT is a versatile SAT/MaxSAT solver for hybrid Boolean constraints.

The types of constraints include: CNF (-or), XOR, cardinality constraints and NAE (not all equal).

Paper: FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints https://arxiv.org/abs/1912.01032 (AAAI-2020)

If you have questions or thoughts regarding the tool or this work, please contact zhiwei@rice.edu.

---

Required environment

python with Scipy

Basic usage

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, in FourierSAT_Github_AIJ/, run:

python FourierSAT.pu sample.cnf --timelimit 10 --tolerance 1 --cpus 2 --verbose 1

Input: Extended DIMACS Format

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"

Output

-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)