Commit 869738e1 authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

balanced_cnf in bin, removed examples

parent 22b6cb47
......@@ -41,6 +41,7 @@ su_add_exec(rhbdmc_compile true true)
su_add_pthread (rhbdmc_compile)
su_add_exec(triple_cnf false false)
su_add_exec(balanced_cnf false false)
su_add_exec(gdbasis false false)
# add_executable (horn_uniform_pcgen horn_uniform_pcgen.cpp)
......
......@@ -9,8 +9,7 @@
#include <csignal>
#include <iostream>
#include <cxxopts.hpp>
#include <optional>
#include "assign.h"
#include "logstream.h"
......@@ -18,76 +17,41 @@
#include "pccomp.h"
#include "prgutil.h"
const std::string prg_name = "balanced_cnf";
const std::string prg_desc =
const std::string SUBool::kPrgName = "balanced_cnf";
const std::string SUBool::kPrgDesc =
"Generates special CNF with 3n variables and all prime implicates having n "
"positive, n negative and n missing literals. Then minimizes it.";
"positive, n negative and n missing literals.";
struct config_t
{
std::string output_file;
unsigned verbosity; // 0 means no output
unsigned n;
bool minimize;
std::string output_file{};
unsigned n{2};
};
void
dump_config(const config_t &conf, unsigned level)
{
SUBool::logs.TLog(level) << "Configuration:" << std::endl;
SUBool::logs.TLog(level)
<< "\toutput_file: " << conf.output_file << std::endl;
SUBool::logs.TLog(level) << "\tverbosity: " << conf.verbosity << std::endl;
SUBool::logs.TLog(level) << "\tn: " << conf.n << std::endl;
SUBool::logs.TLog(level) << "\tminimize: " << conf.minimize << std::endl;
SUBool::logs.DumpValue("\t", level, "output_file", conf.output_file);
SUBool::logs.DumpVerbosity("\t", level);
SUBool::logs.DumpValue("\t", level, "n", conf.n);
}
int
parse_arguments(int argc, char *argv[], config_t &conf)
std::optional<config_t>
parse_arguments(int argc, char *argv[])
{
try
{
cxxopts::Options options(prg_name, prg_desc);
options.positional_help("[input [output]]");
options.add_options()("h,help", "Print help")(
"v,version", "Print version info")("b,verbosity",
"Verbosity level of the log which is written to standard output."
" 0 means no log is written, however messages of glucose can still "
"appear.",
cxxopts::value<unsigned>(conf.verbosity)
->default_value(SUBool::LogStream::kMaxLogLevels))("o,output",
"Output file with the encoding CNF in DIMACS format",
cxxopts::value<std::string>(conf.output_file))("n",
"The number of variables is 3n",
cxxopts::value<unsigned>(conf.n)->default_value("2"))("m,minimize",
"Run minimization before output",
cxxopts::value<bool>(conf.minimize)->default_value("false"));
options.parse_positional({"output", "positional"});
auto result = options.parse(argc, argv);
if (result.count("help"))
{
std::cout << options.help() << std::endl;
return 1;
}
if (result.count("version"))
{
SUBool::print_version(std::cout, prg_name, prg_desc);
return 1;
}
if (result.count("positional"))
{
SUBool::logs.TLog(0) << "Multiple files passed as parameters, ";
SUBool::logs.TLog(0) << "only output file is allowed" << std::endl;
SUBool::logs.TLog(0) << options.help() << std::endl;
return 1;
}
}
catch (const cxxopts::OptionException &e)
config_t conf;
SUBool::PrgOptions opts;
opts.SinglePositional({&conf.output_file, "output"});
po::options_description desc("Configuration options");
desc.add_options()("block-size,n",
po::value<unsigned>(&conf.n)->default_value(conf.n),
"The number of variables is 3n");
if (!opts.Parse(argc, argv))
{
std::cerr << "Error parsing options: " << e.what() << std::endl;
return 1;
return {};
}
return 0;
return conf;
}
void
......@@ -130,54 +94,27 @@ generate(unsigned n)
return SUBool::CNF(std::move(clauses));
}
SUBool::CNF
minimize(SUBool::CNF cnf)
{
SUBool::PCComp comp(std::move(cnf), SUBool::PCComp::Config(), SUBool::logs);
if (comp.Minimize() != SUBool::AbsIncrementalComp::RESULT::COMPILED)
{
throw SUBool::FailureException("minimize", "Minimization failed!");
}
return std::move(comp).CurrentCNF();
}
int
main(int argc, char *argv[])
{
config_t conf;
int r = parse_arguments(argc, argv, conf);
if (r != 0)
auto conf = parse_arguments(argc, argv);
if (!conf)
{
return r;
return 1;
}
SUBool::logs.mVerbLevel = conf.verbosity;
std::signal(SIGTERM, term_func);
std::signal(SIGQUIT, term_func);
std::signal(SIGINT, term_func);
dump_config(conf, 0);
auto cnf = generate(conf.n);
dump_config(*conf, 0);
auto cnf = generate(conf->n);
try
{
if (conf.minimize)
{
cnf = minimize(std::move(cnf));
}
SUBool::output(conf.output_file, cnf);
}
catch (SUBool::FailureException &e)
{
SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::NONE)
<< "[FAILED]" << e.what() << std::endl;
SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::NONE)
<< "No output written" << std::endl;
return 1;
SUBool::output(conf->output_file, cnf);
}
catch (SUBool::IOException &e)
{
SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::NONE)
<< e.what() << std::endl;
SUBool::logs.TLog(SUBool::LogStream::LOG_LEVEL::NONE)
<< "No output written" << std::endl;
SUBool::logs.TLog(0) << e.what() << std::endl;
SUBool::logs.TLog(0) << "No output written" << std::endl;
return 2;
}
return 0;
......
#The following paths need to be modified to correct ones
SUBool_LIBDIR=../build/lib
SUBool_INCLUDE=../lib
Glucose_TOP=${GLUCOSE_HOME}
SUBool_LIB=subool
Glucose_LIB=_release
CC=g++
LD=g++
CFLAGS=-c -Wall -O3 --std=c++11 -I $(SUBool_INCLUDE) -I $(Glucose_TOP)
LDFLAGS=-L $(SUBool_LIBDIR) -l $(SUBool_LIB) -L $(Glucose_TOP)/simp -l$(Glucose_LIB)
all: balanced_cnf
clean:
-+ rm -f balanced_cnf.o balanced_cnf
%.o: %.cpp
$(CC) $(CFLAGS) -o $@ $<
balanced_cnf.o: balanced_cnf.cpp
balanced_cnf: balanced_cnf.o
$(LD) -rdynamic $< -o $@ $(LDFLAGS)
pccheck [OPTION...] [input [output]]
TODO: Allow only input file, output file should be passed with -e option
UNIT REFUTATION COMPLETENESS
-u, --uc Aim for unit refutation completeness instead
of propagation completeness.
ONE PROVABILITY
-1, --one-prove arg What kind of encoding should be used for
1-provability.
--log-enc-opts arg Options to logarithmic encoding modifying
some of its features. It is a string composed of
comma separated option strings which specifies
which additional parts should be added to the
encoding. Possible values specifying the
features are: amf -- AMO on fire variables for
each derived literal will be part of the
encoding. cex -- Comparison exclusivity clauses will
be added to the encoding. flm -- Clauses
forcing linear order when the number of levels is
maximum will be added to the encoding. cml -- A
variable is contradictory if and only its
level has all ones. (default: amf,cex,flm,cml)
--impl-system arg Determines the type of an implication system
to be used when required by encoding of
empowerement or 1-provability. 'none' -- no
implication system (must not be used with any choice
of one-prove and empower options which requires
an implication system. Should be used with
other option combinations. 'drenc' -- use plain
dual rail encoding. 'irredundant' -- make the
dual rail encoding irredundant (both body and
right). 'gdbasis' -- use GD basis of the dual
rail encoding. 'gdbasis_right_irred' --
construct GD basis and make it right irredundant.
'body_minimal' -- make the dual rail encoding
body minimal (like GD basis but without left
saturation). 'body_minimal_irred' -- make the
dual rail encoding body minimal and right
irredundant. The default value depends on other
options, it is none for the combination of options
one-prove and empower which do not require any
implication system, and body_minimal_irred
for the option combination which needs an
implication system. (default: none)
-l, --level arg Maximum level of unit propagation for
1-provability. In case of compilation, the
compilation stops when no empowering implicate with
level at most l is found. Value 0 means, the level
is not bounded. Note that in case of
quadratic encoding this is really the maximum level,
in case of logarithmic encoding this is the
number of bits used to encode a number of level.
In case of choice -1 4 when the minimum of
quadratic and logarithmic encoding is considered,
the level bounds the number of level of the
quadratic encoding while the number of levels
of the logarithmic encoding is bounded to the
logarithm of the parameter rounded up.
(default: 0)
GENERAL OPTIONS
-d, --dump Back mapping of variables (names) are used
wherever possible
-e, --encode Do not check, just write the encoding to the
output file
PREPROCESSING
-n, --no-up-backbones Do NOT perform propagation of literals which
can be derived by unit propagation from the
input formula. This is useful for checking the
construction of an encoding.
EMPOWEREMENT
-w, --empower arg What kind of encoding should be used for
empowerment. 0 = quadratic encoding with
equivalences. 1 = quadratic encoding with implications.
2 = one level encoding. (default: 2)
TIMEOUTS
-t, --timeout arg Total timeout for the computation in seconds as a
fractional number. After this amount of seconds,
the process finishes. Value t<=0.0 means no
timeout. The timer uses CLOCK_REALTIME. (default:
-1.000000)
--emp-timeout arg Timeout for a single SAT call which looks for
an empowering implicate. The timeout is in
seconds as a fractional number. (default:
-1.000000)
--emp-timeout-level-base arg
This parameter together with
emp-timeout-level-factor allows to set the timeout for a
single SAT which looks for an empowering implicate
depending on the number of levels of unit
propagation allowed in the encoding. Denote the
value of emp-timeout-level-base as B and the
value of emp-timeout-level-factor as F. For a
level L which is neither 0 nor maximum (i.e. the
number of variables), the timeout is set as
B+F*L. If the value is higher than emp-timeout,
then the value of emp-timeout is used instead.
The timeout is passed as a fractional number
specifying the number of seconds. (default:
-1.000000)
--emp-timeout-level-factor arg
This parameter together with
emp-timeout-level-base allows to set the timeout for a single
SAT which looks for an empowering implicate
depending on the number of levels of unit
propagation allowed in the encoding (see the
description of emp-timeout-level-base for more
details). If the value is higher than emp-timeout,
then the value of emp-timeout is used instead.
The timeout is passed as a fractional number
specifying the number of seconds. (default:
0.000000)
SOLVERS
--pccheck-solver arg Solver to be used for the PC check. glucose =
use glucose, kissat = use kissat. (default:
glucose)
CARDINALITY CONSTRAINTS
--amo arg Which encoding to use for the at-most-one
constraint. repr = use the representation, seq =
use the sequential encoding. (default: repr)
--exactly-one arg Which encoding to use for the exactly-one
constraint. repr = use the representation, split
= use the splitting encoding. (default: repr)
pccompile [OPTION...] [input [output]]
Algorithm Selection
-a, --algorithm arg The compilation algorithm. 'incremental' -- a
heuristic algorithm based on incremental
adding empowering implicates, allows preprocessing
and inprocessing. This works in both kinds of
goals (PC/UC). 'learning' -- an algorithm
based on the algorithm for learning a Horn
formula through equivalence and closure queries
(Arias et al. 2015). This works only for goal PC.
If goal is UC, the program ends with error.
Other parameters are used appropriately.
(default: incremental)
UNIT REFUTATION COMPLETENESS
-u, --uc Aim for unit refutation completeness instead
of propagation completeness.
--interleave-pc In case of compilation to UC, interleave
encodings for UC and PC.
LEARNING ALGORITHM
--use-empty-initial-hypothesis
Use empty initial hypothesis in the learning
algorithm. If not set, the preprocessed input
CNF is used as an initial hypothesis.
--initial-negatives arg How the initial negative examples in the
learning algorithm should be produced. The option
specifies how the negatives for each clause in
the preprocessed CNF are created. For a
clause C, the possible options are as follows:
'single_empowering' - Only one negative is
produced (C without a literal with respect to which C
is empowering), 'all' - All negatives are
produced (C without l fo every literal l in C),
'all_empowering' - For every literal l in C if
C is empowering with respect to l, then C
without l is produced.'gd_basis' - GD basis of the
dual rail encoding of the prepreocessed CNF
is computed, the bodies in the GD basis are
used as an initial list of
negatives.'body_minimal' - body minimal representation for the dual
rail encoding of the preprocessed CNF is
computed. The bodies in this representation are
used as an initial list of negatives. (default:
all_empowering)
SOLVERS
--pccheck-solver arg Solver to be used for the PC check. glucose =
use glucose, kissat = use kissat. (default:
glucose)
ONE PROVABILITY
-1, --one-prove arg What kind of encoding should be used for
1-provability.
--log-enc-opts arg Options to logarithmic encoding modifying
some of its features. It is a string composed of
comma separated option strings which specifies
which additional parts should be added to the
encoding. Possible values specifying the
features are: amf -- AMO on fire variables for
each derived literal will be part of the
encoding. cex -- Comparison exclusivity clauses will
be added to the encoding. flm -- Clauses
forcing linear order when the number of levels is
maximum will be added to the encoding. cml -- A
variable is contradictory if and only its
level has all ones. (default: amf,cex,flm,cml)
--impl-system arg Determines the type of an implication system
to be used when required by encoding of
empowerement or 1-provability. 'none' -- no
implication system (must not be used with any choice
of one-prove and empower options which requires
an implication system. Should be used with
other option combinations. 'drenc' -- use plain
dual rail encoding. 'irredundant' -- make the
dual rail encoding irredundant (both body and
right). 'gdbasis' -- use GD basis of the dual
rail encoding. 'gdbasis_right_irred' --
construct GD basis and make it right irredundant.
'body_minimal' -- make the dual rail encoding
body minimal (like GD basis but without left
saturation). 'body_minimal_irred' -- make the
dual rail encoding body minimal and right
irredundant. The default value depends on other
options, it is none for the combination of options
one-prove and empower which do not require any
implication system, and body_minimal_irred
for the option combination which needs an
implication system. (default: none)
-l, --level arg Maximum level of unit propagation for
1-provability. In case of compilation, the
compilation stops when no empowering implicate with
level at most l is found. Value 0 means, the level
is not bounded. Note that in case of
quadratic encoding this is really the maximum level,
in case of logarithmic encoding this is the
number of bits used to encode a number of level.
In case of choice -1 4 when the minimum of
quadratic and logarithmic encoding is considered,
the level bounds the number of level of the
quadratic encoding while the number of levels
of the logarithmic encoding is bounded to the
logarithm of the parameter rounded up.
(default: 0)
PREPROCESSING
-r, --preprocess arg Method of preprocessing. 0 = No
preprocessing. 1 = Minimize the formula before compilation.
2 = First make CNF prime with respect to
1-provability, then minimize. 3 = First make CNF
prime and then minimize. 4 = Only make CNF
prime with respect to 1-provability, no
minimization. 5 = Only make CNF prime, no minimization.
(default: 3)
--no-backbone-propagation
Do not perform backbone propagation before
preprocessing.
RANDOM PC CHECKS
-S, --seed arg Initial random seed. Current time is used, if
the seed is not provided explicitly.
--pccheck-random-rounds arg
Number of rounds during one random check of
PC. (default: 100)
--pccheck-random-budget arg
How many times unsucessful random PC check
should be repeated. 0 means no random check is
ever performed. (default: 10)
--pccheck-random-budget-inc arg
Increase of the current budget in case a
random negative example was successfully found. 0
means no increase. (default: 1)
EMPOWEREMENT
-w, --empower arg What kind of encoding should be used for
empowerment.
SIMPLIFICATION
-m, --minimize Minimize the compiled cnf.
--minimize-method arg Minimization method. Possible values: full --
full minimization (with the full CNF)
simple_incremental -- sort in increasing order by
sizes and then add nonabsorbed clauses in this
sequence, starting with the empty CNF, the
result is not necessarily fully minimized.
full_incremental -- same as simple_incremental, in
addition, now after a specific length of clauses
is processed, they are reprocessed again as in
full minimization. Only after then longer
clauses are considered. The result is not
necessarily fully minimized, but it can be
significantly smaller than in case of
simple_incremental. (default: full)
-s, --simp-steps arg Number of empowering clauses after which a
heuristic simplification of the current formula
proceeds. Zero (0) means that no
simplification is made during the compilation. However
final minimization shall proceed depending on
presence of -m option. (default: 50)
--no-level-simplify Do not perform simplification when the number
of levels of unit propagation increases.
TIMEOUTS
-t, --timeout arg Total timeout for the computation in seconds as a
fractional number. After this amount of seconds,
the process finishes. Value t<=0.0 means no
timeout. The timer uses CLOCK_REALTIME. (default:
-1.000000)
--emp-timeout arg Timeout for a single SAT call which looks for
an empowering implicate. The timeout is in
seconds as a fractional number. (default:
-1.000000)
--emp-timeout-level-base arg
This parameter together with
emp-timeout-level-factor allows to set the timeout for a
single SAT which looks for an empowering implicate
depending on the number of levels of unit
propagation allowed in the encoding. Denote the
value of emp-timeout-level-base as B and the
value of emp-timeout-level-factor as F. For a
level L which is neither 0 nor maximum (i.e. the
number of variables), the timeout is set as
B+F*L. If the value is higher than emp-timeout,
then the value of emp-timeout is used instead.
The timeout is passed as a fractional number
specifying the number of seconds. (default:
-1.000000)
--emp-timeout-level-factor arg
This parameter together with
emp-timeout-level-base allows to set the timeout for a single
SAT which looks for an empowering implicate
depending on the number of levels of unit
propagation allowed in the encoding (see the
description of emp-timeout-level-base for more
details). If the value is higher than emp-timeout,
then the value of emp-timeout is used instead.
The timeout is passed as a fractional number
specifying the number of seconds. (default:
0.000000)
CARDINALITY CONSTRAINTS
--amo arg Which encoding to use for the at-most-one
constraint. repr = use the representation, seq =
use the sequential encoding. (default: repr)
--exactly-one arg Which encoding to use for the exactly-one
constraint. repr = use the representation, split
= use the splitting encoding. (default: repr)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment