meelgroup / gaussmaxhs Goto Github PK

GaussMaxHS, a CNF+XOR MaxSAT solver

License: Other

Makefile 1.17% C++ 92.34% C 0.62% Python 5.06% Shell 0.80%

maxsat cnf xor gauss-elimination gauss-jordan

gaussmaxhs's Introduction

GaussMaxHS, a CNF-XOR MaxSAT solver based on MaxHS

The code uses MiniSat as the SAT solver, CPLEX from IBM as the MIPS solver, MaxHS for MaxSAT solving, and a version of Gauss-Jordan elimination to perform CDCL(T). For our research paper PDF, see here, published at Knowledge Representation and Reasoning (KR) 2021 (Bibtex)

Building and installing

Get CPLEX

You need the CPLEX static libraries to link against. CPLEX is available from IBM under their academic Initiative program. It is free to faculty members and graduate students in academia, see here.

You can apply for their academic initiative program and then then you can download CPLEX and other IBM software.

Configure and Build

Use make config VAR=defn or edit config.mk directly. Required variable settings:

Linux: LINUX_CPLEXLIBDIR=<path to CPLEX library> the directory on your linux system that contains libcplex.a and libilocplex.a (the makefile does a static build). LINUX_CPLEXINCDIR=<path to CPLEX headers>
MacOS: DARWIN_CPLEXLIBDIR=<path to CPLEX library> the directory on your MAC system that contains libcplex.a and libilocplex.a (the makefile does a static build), DARWIN_CPLEXINCDIR=<path to CPLEX headers>

After the above configuration, you can:

make install

How to Run

The system expects a CNF-XOR input, which is the same as the WDIMACS format with the extension that you can add XOR constraints just like with CryptoMiniSat, and the weight must be provided after the 'x'. Note that all XOR constraints must be hard constraints. Furthermore, XOR constraints must be at least 3-long, as 2-long XORs are trivial to write in CNF as two binary constraints.

For example, let's take the following input file:

p wcnf 4 6 10
5 1 2 -3 0
5 1 -2 3 0
5 -1 2 3 0
5 -1 -2 -3 0
x 10 1 2 3 0
x 10 -1 3 4 0

This file contains four variables and six constraints, and promises to give weights with a hard constraint having a weight of 10 (hence the header p wcnf 4 6 10). The first four constraints say that v1 or v2 or NOT v3 = true, v1 or NOT v2 or v3 = true, etc. all being soft constraint with a weight of 5. The last two lines say that v1 XOR x2 = true and v1 XOR v3 XOR v4 = false, both of which have a weight of 10, and are hard constraints.

When you run the tool on the problem above, you get the following output:

git clone https://github.com/meelgroup/gaussmaxhs
cd gaussmaxhs
make
cd build/bin/release
./maxhs input.wcnf
[...]
o 5
s OPTIMUM FOUND
v -1 -2 3 4
[...]

This indicates that the lowest cost has been found, and it's the solution v1=false, v2=false, v3=true, v4=true. The cost of this solution is 5, because one of the soft constraints had to be violated, as together they clash with the first XOR constraint.

Generating Spin Glass and Network Reliability problems

You will find generate-netrel.sh and generate-spin.sh problem generators under the default binary location build/release/bin. You can run these scripts to generate example Spin Glass and Network Reliability problems for you.

To run the generate-netrel.sh script, you will need to extract the files from build/release/bin/network-reliability/net-rel.tar.gz first. The files should all be extracted under build/release/bin/network-reliability/, e.g. one file should be build/release/bin/network-reliability/Net27_90_22_count_118.cnf.

Fuzzing

You can find various fuzzers for the GaussMaxHS system under build/release/bin, the default binary location. You can run fuzz.sh to fuzz the system against MaxHS without Gauss-Jordan elimination. While this fuzzing is incomplete, it should find most bugs. You will need CryptoMiniSat5 installed, as the script uses CryptoMiniSat to check for errors with GJE.

gaussmaxhs's People

Contributors

Stargazers

Watchers

Forkers

vuphan314

gaussmaxhs's Issues

An issue with XOR

It seems to me that gaussmaxhs does not recognize the polarity of the XOR constraints. I tested the following toy example:

p wcnf 3 2 2
x 2 1 2 3 0
x 2 1 2 -3 0

The hard constraints are UNSAT but gaussmaxhs returns the following, which indicates that the instance is SAT. I found that the spin instances seem to not have negated literals in XOR constraints. Thus I am wondering if something is missing. Thanks in advance!

-----------------------------------------------------------
xor added to vec:[ 1 2 3 ] (3)
xor added to vec:[ 1 2 -3 ] (3)
c Instance: ../../../testxor.cnf
c Dimacs Vars: 3
c Dimacs Clauses: 2
c HARD: #Clauses = 2, Total Lits = 6, Ave Len = 3
c SOFT: #Clauses = 0, Total Lits = 0, Ave Len = -nan
c Total Soft Clause Weight (+ basecost): 0 (+ 0), Dimacs Top = 2
c SOFT%: 0%
c #distinct weights: 0, mean = 0, std. dev = 0, min = 0, max = 0
c Total Clauses: 2
c Parse time: 0.000121
c Wcnf Space Required: 0MB
c ================================
c transitionWts = [ ] (0)
c WCNF hardened 0 soft clauses
c WCNF units: found 0 units
c WCNF units: removed 0 hard clauses with 0 lits
c WCNF units: removed 0 soft clauses with 0 lits
xor added to vec:[ 1 2 3 ] (3)
xor added to vec:[ 1 2 -3 ] (3)
c WCNF found 0 redundant hards and 0 duplicate or subsumed softs
c WCNF mutexes: #mutexes found = 0
c WCNF mx finder used 0 calls to UP engine
c WCNF mutexes: original #softs 0 #softs after mx-transforms 0
c WCNF mutexes: reduction in softs 0
c After WCNF Simplification
c HARD: #Clauses = 2, Total Lits = 6, Ave Len = 3
c SOFT: #Clauses = 0, Total Lits = 0, Ave Len = -nan
c Total Soft Clause Weight (+ basecost): 0 (+ 0), Dimacs Top = 2
c #distinct weights: 0, mean = 0, std. dev = 0, min = 0, max = 0
c Total Clauses: 2
c Wcnf Space Required: 2.4e-05MB
c ================================
c Muser: Vars of hards = 3 vars to be frozen = 0
c Muser Preprocess eliminated 0 variables. took 2e-06 sec.
c Using IBM CPLEX version 20.1.0.0 under IBM's Academic Initiative licencing program
c Total used vars = 3 vars to be frozen = 0
c MiniSat Preprocess eliminated 0 variables. took 3e-06 sec.
c Before solving sat solver has 0 clauses and 0 learnts
c Init Bnds: SAT Time 1e-05
c New UB found 0
c Elapsed time 4.6e-05
c Solved by Init Bnds.
o 0
s OPTIMUM FOUND
v -1 -2 -3
xor added to vec:[ 1 2 3 ] (3)
xor added to vec:[ 1 2 -3 ] (3)
c Solved: Number of falsified softs = 0
c CPLEX: #constraints 0
c CPLEX: Avg constraint size -nan
c CPLEX: #non-core constraints 0
c CPLEX: Ave non-core size -nan
c SAT: #calls 1
c SAT: Total time 1e-05
c SAT: #muser calls 0 (-nan % successful)
c SAT: Minimize time 0 (0%)
c SAT: Avg constraint minimization -nan
c CPLEX: #calls 0
c CPLEX: Total time 0
c GREEDY: #calls 0
c GREEDY: Total time 0
c LP-Bounds: Hardened 0 softs 0 because not in cplex
c LP-Bounds: Relaxed 0 softs
c LP-Bounds: Total time 0
c LP-Bounds: #calls 0
c CPLEX: #calls 0
c CPLEX: Total time 0
c MEM MB: 42
c CPU: 0.0019
---------------------------------------------------------------------------------

XOR clauses

Hi!

I tried to use this solver for inputs that look like this:

p wcnf 6 15 21
x 21 1 0
x 21 2 0
x 21 3 0
x 21 4 0
x 21 5 0
x 21 6 0
x 21 2 5 0
x 21 2 3 4 5 6 0
x 21 1 2 4 5 6 0
x 21 1 3 4 5 0
x 21 2 3 5 0
x 21 4 5 6 0
x 21 4 5 6 0
x 21 2 5 6 0
x 21 2 3 4 5 6 0

Because XOR constraints must be at least 3-long, I transformed the above input in:

wcnf 22 16 38
x 38 1 2000 2001 0
x 38 2 2002 2003 0
x 38 3 2004 2005 0
x 38 4 2006 2007 0
x 38 5 2008 2009 0
x 38 6 2010 2011 0
x 38 2 5 2012 0
x 38 2 3 4 5 6 0
x 38 1 2 4 5 6 0
x 38 1 3 4 5 0
x 38 2 3 5 0
x 38 2013 2014 2015 0
x 38 4 5 6 0
x 38 4 5 6 0
x 38 2 5 6 0
x 38 2 3 4 5 6 0

where I added some new variables (which I no longer use elsewhere) in order to make an XOR constraint of length 3.

This idea works for small inputs, but when I try to apply the same method on bigger inputs (for example, 500 variables and 700 constraints), I get a segmentation fault error message. I leave an input file for this case here: https://filetransfer.io/data-package/iTkNZKGW#link

Do you have any suggestions on what I could do in this case? Thank you.

Hard XOR clause violated

Hi @msoos,

GaussMaxHS appears to violate a hard clause:

cat f.wcnf

p wcnf 3 1 4
x 4 1 2 3 0

Output:

gaussmaxhs f.wcnf -verb=0

c MaxHS 3.0.0
xor added to vec:[ 1 2 3 ] (3)
c Solved by Init Bnds.
o 0
s OPTIMUM FOUND
v -1 -2 -3

This may be related to issue #1.

Thank you.

Hard XOR constraints violated

Hi!

I try to use GaussMaxHS to solve a problem with 1600 variables, including 80 exactly-one constraint (hard), 30400 clauses (hard) and 1600 XOR constraints (soft). The XOR constraints are harden using the approach mentioned in "Gaussian Elimination Meets Maximum Satisfiability", section 4.1. At the end, it is encoded as:

p wcnf 3200 96080 1601
x 1601 3 4 6 8 10 13 14 16 17 21 22 25 28 29 30 31 32 33 ...
x 1601 1 5 6 8 10 11 12 17 21 22 23 24 27 28 29 30 31 34 ...
...
c hard clauses
1601 -16 -48 0
1601 -8 -56 0
...
c soft clauses due to harden XOR
1 -1601 0
1 -1602 0
...

Then GaussMaxHS seems to give the solution very fast. However, the solution seems not to be correct.

0.54/0.65	c Wcnf Space Required: 5MB
0.54/0.65	c ================================
0.54/0.65	c Using IBM CPLEX version 22.1.1.0 under IBM's Academic Initiative licencing program
0.54/0.65	o 0
0.54/0.65	c Solved by Init Bnds.
0.54/0.65	o 0
0.54/0.65	s OPTIMUM FOUND
0.54/0.65	v -1 -2 -3 -4 -5 ...

When the size of the problem is smaller (900 XOR hard constraint, length is 451), GaussMaxHS can give the correct solution. In this problem, is it because the XOR constraints are too large (1600 XOR hard constraint, length is 801)?