initial

.gitignore

@@ -0,0 +1,8 @@
+.vscode/
+__pycache__/
+*.a
+*.o
+makefile
+config.h
+xnfsat
+xnfsat_parallel

FILES

@@ -0,0 +1,13 @@
+xnfsat          executable SAT solver
+xnfsat_parallel executable SAT solver simple portfolio version
+main.c          front-end, e.g. dimacs parser, connects to library
+libyals.a       actual library 
+yals.h          library include file
+yals.c          library implementation
+yils.h          internal API calls
+config.c        prints banner (includes configuration)
+config.h        automatically generated from './mkconfig.sh'
+makefile        instantiated from 'makfile.in' by './configure.sh'
+configure.sh    configure script (try './configure -h')
+mkconfig.sh     prints version and compile time information
+makefile.in     makefile template

LICENSE

@@ -0,0 +1,24 @@
+Copyright (c) 2021
+Armin Biere, Johannes Kepler University
+Andreas Fröhlich
+Marijn Heule
+Lilian Liu
+Wojciech Nawrocki
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

README

@@ -0,0 +1,10 @@
+xnfSAT
+
+This is an SLS solver with XOR constraint support based on YalSAT.
+
+To build, run './configure.sh && make'. See also './configure.sh -h',
+particularly the usage of './configure.sh -g' to compile a version
+with debugging, checking and logging support.
+
+This will build both the library 'libyals.a' with its API in file 'yals.h'
+and the stand-alone SAT solver 'xnfsat'.

VERSION

@@ -0,0 +1 @@
+03v-xnfsat-fixed

cflags.h

@@ -0,0 +1,2 @@
+#define YALS_CC "gcc (GCC) 10.2.0"
+#define YALS_CFLAGS "-Wall -Wextra -DNDEBUG -O3"

cnf2xnf/.gitignore

@@ -0,0 +1,9 @@
+cnf2xnf
+xnf2cnf3
+xnf2cnf4
+xnf2cnf5
+xnf2cnf6
+xnf2cnf7
+xnf2cnf8
+extor
+makefile

cnf2xnf/README.md

@@ -0,0 +1,14 @@
+This is a CNF to XNF extractor. To build, try
+
+    ./configure && make
+
+or even
+
+    ./configure && make test
+
+You can then for instance extract a CNF with cutting number 4 through
+
+    ./cnf2xnf4 cnfs/xor1.cnf cnfs/xor1.xnf
+
+Armin Biere
+Februrary 2021