Skip to content

Add reduction using SAT and QBF solvers #407

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 6 commits into
base: devel
Choose a base branch
from
Draft

Add reduction using SAT and QBF solvers #407

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
6c32178
Add reduction using SAT and QBF solvers
notValord Apr 17, 2024
d14f538
Fix static analysis issues and rework parsing of the solver output.
notValord Jun 1, 2024
bb25d13
Remove needless library.
notValord Jun 1, 2024
35f77ce
Merge branch 'devel' into reduction_using_solvers to resolve conflicts.
notValord Jun 1, 2024
6c531b4
Add unistd.h as it is required by compiler.
notValord Jun 1, 2024
981aa05
Add tests for reduction using solvers.
notValord Jun 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Binary file added 3rdparty/solvers/MiniSat.14_linux
View file
Open in desktop
Binary file not shown.
Binary file added 3rdparty/solvers/caqe
View file
Open in desktop
Binary file not shown.
55 changes: 49 additions & 6 deletions include/mata/nfa/nfa.hh
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@
#include <utility>
#include <vector>
#include <queue>
#include <unistd.h>

#include "mata/alphabet.hh"
#include "mata/parser/parser.hh"
Expand Down Expand Up @@ -530,20 +531,54 @@ Nfa minimize(const Nfa &aut, const ParameterMap& params = {{ "algorithm", "brzoz
*/
Nfa determinize(const Nfa& aut, std::unordered_map<StateSet, State> *subset_map = nullptr);

/**
* @brief A CNF transformation to the provided clause in form of disjunctions of long and-not clauses,
* utilized for reduction using SAT and QBF solvers, printed to output
* @param[in] input Vector with the clause in DNF form to transform
* @param[in] max_index Starting index of free variables used for new generated variables
* @param[in] output Output stream
* @return The first variable index that was not utilized
*/
size_t reduction_tseytin(const std::vector <int>& input, size_t max_index, std::ostream& output);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should this method be called tseytin_transformation() instead of a reduction? Furthermore, if I am seeing right, this method does not use the underlying automaton in any way, so it can be a utility function, not even a method o
NFA, no? Stored somewhere in utils/ folder, probably.


/**
* @brief Experimental reduction using sat solver MiniSat with idea of creating minimal nondeterministic automaton,
* is not possible to use for normal sized automata (around 10 states max), requires the alphabet of input automaton
* to be a continuous sequence of numbers strating from 0
* @param[in] aut Automaton to reduce
* @param[in] params Optional pamaters to control the reduction:
* - "solver": "sat"/"sat_nfa" (sat for the dfa complete automaton with single initial state)
* @param[in] debug Flag for debug output as the reduction can take some time to get the info about the current status
* @return Reduced automaton
*/
Nfa reduce_sat(const Nfa &aut, const ParameterMap& params = {{"solver", "sat"}}, bool debug = false);
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think that both the specific reduction algorithms should be hidden behind the general reduce function. That is, they should not be in the public API for Nfa, and be only accessible in the anonymous namespace of operations.cc. Or, since we are starting to have way to many reduction algorithms, we could create a new source file specifically for reductions reduction.cc with potentially a new header file reduction.hh which can be included when one want to call the specific reduction algorithms. Creating a new source and header files seems like the best approach to me.


/**
* @brief Experimental reduction using qbf solver CAQE with idea of creating minimal nondeterministic automaton,
* is not possible to use for normal sized automata (around 10 states max), requires the alphabet of input automaton
* to be a continuous sequence of numbers strating from 0
* @param[in] aut Automaton to reduce
* @param[in] debug Flag for debug output as the reduction can take some time to get the info about the current status
* @return Reduced automaton
*/
Nfa reduce_qbf(const Nfa &aut, bool debug = false);

/**
* @brief Reduce the size of the automaton.
*
* @param[in] aut Automaton to reduce.
* @param[out] state_renaming Mapping of original states to reduced states.
* @param[in] params Optional parameters to control the reduction algorithm:
* - "algorithm": "simulation", "residual",
* and options to parametrize residual reduction, not utilized in simulation
* - "algorithm": "simulation", "residual", "solvers",
* options to parametrize residual reduction, not utilized in other reductions
* - "type": "after", "with",
* - "direction": "forward", "backward".
* - "direction": "forward", "backward",
* options to parametrize reduction using solvers, not utilized in other reductions
* - "solver": "sat"/"sat_nfa"/"qbf".
* @return Reduced automaton.
*/
Nfa reduce(const Nfa &aut, StateRenaming *state_renaming = nullptr,
const ParameterMap& params = {{ "algorithm", "simulation" }, { "type", "after" }, { "direction", "forward" } });
const ParameterMap& params = {{ "algorithm", "simulation" }, { "type", "after" }, { "direction", "forward" }, {"solver", "nfa"} });

/**
* @brief Checks inclusion of languages of two NFAs: @p smaller and @p bigger (smaller <= bigger).
Expand Down Expand Up @@ -574,6 +609,8 @@ inline bool is_included(const Nfa& smaller, const Nfa& bigger, const Alphabet* c
return is_included(smaller, bigger, nullptr, alphabet, params);
}

// static default value for empty run pair
static std::pair<Run*, Run*> default_runs(nullptr, nullptr);
/**
* @brief Perform equivalence check of two NFAs: @p lhs and @p rhs.
*
Expand All @@ -582,10 +619,13 @@ inline bool is_included(const Nfa& smaller, const Nfa& bigger, const Alphabet* c
* @param[in] alphabet Alphabet of both NFAs to compute with.
* @param[in] params[ Optional parameters to control the equivalence check algorithm:
* - "algorithm": "naive", "antichains" (Default: "antichains")
* @param[out] default_runs Optional parameter for intersection runs to return the found word
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it is wasteful to pass by reference and have a statically initialized pair of pointers (which will get modified when the equivalence check gets run the second time -- therefore, they will no longer be the default runs). A pointer to a pair of runs should be used instead, default initialized to nullptr.

However, I think the global variable for default runs should be removed entirely and the parameter here should be a pointer default initialized to nullptr.

* that differs the input automata, used for solver reduction
* @return True if @p lhs and @p rhs are equivalent, false otherwise.
*/
bool are_equivalent(const Nfa& lhs, const Nfa& rhs, const Alphabet* alphabet,
const ParameterMap& params = {{ "algorithm", "antichains"}});
const ParameterMap& params = {{ "algorithm", "antichains"}},
std::pair<Run*, Run*>& runs = default_runs);

/**
* @brief Perform equivalence check of two NFAs: @p lhs and @p rhs.
Expand All @@ -602,9 +642,12 @@ bool are_equivalent(const Nfa& lhs, const Nfa& rhs, const Alphabet* alphabet,
* @param[in] rhs Second automaton to concatenate.
* @param[in] params Optional parameters to control the equivalence check algorithm:
* - "algorithm": "naive", "antichains" (Default: "antichains")
* * @param[out] default_runs Optional parameter for intersection runs to return the found word
* that differs the input automata, used for solver reduction
* @return True if @p lhs and @p rhs are equivalent, false otherwise.
*/
bool are_equivalent(const Nfa& lhs, const Nfa& rhs, const ParameterMap& params = {{ "algorithm", "antichains"}});
bool are_equivalent(const Nfa& lhs, const Nfa& rhs, const ParameterMap& params = {{ "algorithm", "antichains"}},
std::pair<Run*, Run*>& runs = default_runs);

// Reverting the automaton by one of the three functions below,
// currently simple_revert seems best (however, not tested enough).
Expand Down
Loading
Loading