academic/kissat: Added (SAT solver).

Signed-off-by: Willy Sudiarto Raharjo <willysr@slackbuilds.org>
This commit is contained in:
alan_NaverOsa@lavSaPbiAtM.com 2024-04-14 10:59:06 +07:00 committed by Willy Sudiarto Raharjo
parent 5118f7868b
commit df4e060a18
No known key found for this signature in database
GPG key ID: 3F617144D7238786
4 changed files with 158 additions and 0 deletions

16
academic/kissat/README Normal file
View file

@ -0,0 +1,16 @@
Kissat is a "keep it simple and clean bare metal SAT solver" written
in C. It is a port of CaDiCaL back to C with improved data
structures, better scheduling of inprocessing and optimized
algorithms and implementation.
Coincidentally "kissat" also means "cats" in Finnish.
You can get more information about Kissat in the last solver
description for the SAT Competition 2022:
Armin Biere and Mathias Fleury. Gimsatul, IsaSAT and Kissat entering
the SAT Competition 2022. In Proc. of SAT Competition 2022 - Solver
and Benchmark Descriptions, Tomas Balyo, Marijn Heule, Markus Iser,
Matti Järvisalo, Martin Suda (editors), vol. B-2022-1 of Department
of Computer Science Report Series B, pages 10-11, University of
Helsinki, 2022.

View file

@ -0,0 +1,113 @@
#!/bin/bash
# Slackware build script for kissat
# Copyright Caterino Tommaso, T.O.P. 2024 USA
# All rights reserved.
#
# Redistribution and use of this script, with or without modification, is
# permitted provided that the following conditions are met:
#
# 1. Redistributions of this script must retain the above copyright
# notice, this list of conditions and the following disclaimer.
#
# THIS SOFTWARE IS PROVIDED BY THE AUTHOR "AS IS" AND ANY EXPRESS OR IMPLIED
# WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF
# MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO
# EVENT SHALL THE AUTHOR BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
# SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
# PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS;
# OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY,
# WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR
# OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF
# ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
cd $(dirname $0) ; CWD=$(pwd)
PRGNAM=kissat
VERSION=${VERSION:-3.1.1}
BUILD=${BUILD:-1}
TAG=${TAG:-_SBo}
PKGTYPE=${PKGTYPE:-tgz}
if [ -z "$ARCH" ]; then
case "$( uname -m )" in
i?86) ARCH=i586 ;;
arm*) ARCH=arm ;;
*) ARCH=$( uname -m ) ;;
esac
fi
if [ ! -z "${PRINT_PACKAGE_NAME}" ]; then
echo "$PRGNAM-$VERSION-$ARCH-$BUILD$TAG.$PKGTYPE"
exit 0
fi
TMP=${TMP:-/tmp/SBo}
PKG=$TMP/package-$PRGNAM
OUTPUT=${OUTPUT:-/tmp}
if [ "$ARCH" = "i586" ]; then
SLKCFLAGS="-O2 -march=i586 -mtune=i686"
LIBDIRSUFFIX=""
elif [ "$ARCH" = "i686" ]; then
SLKCFLAGS="-O2 -march=i686 -mtune=i686"
LIBDIRSUFFIX=""
elif [ "$ARCH" = "x86_64" ]; then
SLKCFLAGS="-O2 -fPIC"
LIBDIRSUFFIX="64"
elif [ "$ARCH" = "aarch64" ]; then
SLKCFLAGS="-O2 -fPIC"
LIBDIRSUFFIX="64"
else
SLKCFLAGS="-O2"
LIBDIRSUFFIX=""
fi
set -e
rm -rf $PKG
mkdir -p $TMP $PKG $OUTPUT
cd $TMP
rm -rf $PRGNAM-rel-$VERSION
tar xvf $CWD/$PRGNAM-rel-$VERSION.tar.gz
cd $PRGNAM-rel-$VERSION
chown -R root:root .
find -L . \
\( -perm 777 -o -perm 775 -o -perm 750 -o -perm 711 -o -perm 555 \
-o -perm 511 \) -exec chmod 755 {} \+ -o \
\( -perm 666 -o -perm 664 -o -perm 640 -o -perm 600 -o -perm 444 \
-o -perm 440 -o -perm 400 \) -exec chmod 644 {} \+
CFLAGS="$SLKCFLAGS" \
CXXFLAGS="$SLKCFLAGS" \
./configure
cd build
make
cd ..
mkdir -p $PKG/usr/bin $PKG/usr/lib${LIBDIRSUFFIX}
cp -a build/kissat $PKG/usr/bin/
cp -a build/libkissat.a $PKG/usr/lib${LIBDIRSUFFIX}/
rm -f $PKG/{,usr/}lib${LIBDIRSUFFIX}/*.la
find $PKG -print0 | xargs -0 file | grep -e "executable" -e "shared object" | grep ELF \
| cut -f 1 -d : | xargs strip --strip-unneeded 2> /dev/null || true
rm -f $PKG/usr/info/dir
find $PKG -name perllocal.pod -o -name ".packlist" -o -name "*.bs" | xargs rm -f || true
mkdir -p $PKG/usr/doc/$PRGNAM-$VERSION
cp -a \
CONTRIBUTING LICENSE NEWS.md README.md VERSION \
$PKG/usr/doc/$PRGNAM-$VERSION
cat $CWD/$PRGNAM.SlackBuild > $PKG/usr/doc/$PRGNAM-$VERSION/$PRGNAM.SlackBuild
mkdir -p $PKG/install
cat $CWD/slack-desc > $PKG/install/slack-desc
cd $PKG
/sbin/makepkg -l y -c n $OUTPUT/$PRGNAM-$VERSION-$ARCH-$BUILD$TAG.$PKGTYPE

View file

@ -0,0 +1,10 @@
PRGNAM="kissat"
VERSION="3.1.1"
HOMEPAGE="https://github.com/arminbiere/kissat"
DOWNLOAD="https://github.com/arminbiere/kissat/archive/refs/tags/rel-3.1.1.tar.gz"
MD5SUM="601d796884d5e9efe2af78dfe77d73ba"
DOWNLOAD_x86_64=""
MD5SUM_x86_64=""
REQUIRES=""
MAINTAINER="Caterino Tommaso, T.O.P."
EMAIL="alan_NaverOsa@lavSaPbiAtM.com (remove capital letters)"

View file

@ -0,0 +1,19 @@
# HOW TO EDIT THIS FILE:
# The "handy ruler" below makes it easier to edit a package description.
# Line up the first '|' above the ':' following the base package name, and
# the '|' on the right side marks the last column you can put a character in.
# You must make exactly 11 lines for the formatting to be correct. It's also
# customary to leave one space after the ':' except on otherwise blank lines.
|-----handy-ruler------------------------------------------------------|
kissat: kissat (International SAT Competition award-winning SAT solver)
kissat: Kissat is a "keep it simple and clean bare metal SAT solver" written
kissat: in C. It is a port of CaDiCaL back to C with improved data
kissat: structures, better scheduling of inprocessing and optimized
kissat: algorithms and implementation.
kissat: Armin Biere and Mathias Fleury. Gimsatul, IsaSAT and Kissat entering
kissat: the SAT Competition 2022. In Proc. of SAT Competition 2022 - Solver
kissat: and Benchmark Descriptions, Tomas Balyo, Marijn Heule, Markus Iser,
kissat: Matti Jarvisalo, Martin Suda (editors), vol. B-2022-1 of Department
kissat: of Computer Science Report Series B, pages 10-11, University of
kissat: Helsinki, 2022