diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..e9225ac --- /dev/null +++ b/.gitignore @@ -0,0 +1,8 @@ +.vscode/ +__pycache__/ +*.a +*.o +makefile +config.h +xnfsat +xnfsat_parallel diff --git a/FILES b/FILES new file mode 100644 index 0000000..9c94b2b --- /dev/null +++ b/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 diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..df5b865 --- /dev/null +++ b/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. diff --git a/README b/README new file mode 100644 index 0000000..8dd748b --- /dev/null +++ b/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'. diff --git a/VERSION b/VERSION new file mode 100644 index 0000000..48b92b9 --- /dev/null +++ b/VERSION @@ -0,0 +1 @@ +03v-xnfsat-fixed diff --git a/cflags.h b/cflags.h new file mode 100644 index 0000000..19126f8 --- /dev/null +++ b/cflags.h @@ -0,0 +1,2 @@ +#define YALS_CC "gcc (GCC) 10.2.0" +#define YALS_CFLAGS "-Wall -Wextra -DNDEBUG -O3" diff --git a/cnf2xnf/.gitignore b/cnf2xnf/.gitignore new file mode 100644 index 0000000..ad3dd12 --- /dev/null +++ b/cnf2xnf/.gitignore @@ -0,0 +1,9 @@ +cnf2xnf +xnf2cnf3 +xnf2cnf4 +xnf2cnf5 +xnf2cnf6 +xnf2cnf7 +xnf2cnf8 +extor +makefile diff --git a/cnf2xnf/README.md b/cnf2xnf/README.md new file mode 100644 index 0000000..b436be9 --- /dev/null +++ b/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 diff --git a/cnf2xnf/cnf2xnf.c b/cnf2xnf/cnf2xnf.c new file mode 100644 index 0000000..b8da9ee --- /dev/null +++ b/cnf2xnf/cnf2xnf.c @@ -0,0 +1,1267 @@ +// Copyright (2021) Armin Biere, JKU LInz. + +#define VERSION "0.3" + +// *INDENT-OFF* + +static const char * usage = +"usage: cnf2xnf [