#include #include using namespace std ; /* begin microsat */ /*********************************************************************[microsat.c]*** The MIT License Copyright (c) 2014-2018 Marijn Heule 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. *************************************************************************************/ #include #include enum { END = -9, UNSAT = 0, SAT = 1, MARK = 2, IMPLIED = 6 }; struct solver { // The variables in the struct are described in the initCDCL procedure int *DB, nVars, nClauses, mem_used, mem_fixed, mem_max, maxLemmas, nLemmas, *buffer, nConflicts, *model, *reason, *falseStack, *msfalse, *first, *forced, *processed, *assigned, *next, *prev, head, res, fast, slow; }; void unassign (struct solver* S, int lit) { S->msfalse[lit] = 0; } // Unassign the literal void restart (struct solver* S) { // Perform a restart (i.e., unassign all variables) while (S->assigned > S->forced) unassign (S, *(--S->assigned)); // Remove all unforced false lits from falseStack S->processed = S->forced; } // Reset the processed pointer void assign (struct solver* S, int* reason, int forced) { // Make the first literal of the reason true int lit = reason[0]; // Let lit be the first literal in the reason S->msfalse[-lit] = forced ? IMPLIED : 1; // Mark lit as true and IMPLIED if forced *(S->assigned++) = -lit; // Push it on the assignment stack S->reason[abs (lit)] = 1 + (int) ((reason)-S->DB); // Set the reason clause of lit S->model [abs (lit)] = (lit > 0); } // Mark the literal as true in the model void addWatch (struct solver* S, int lit, int mem) { // Add a watch pointer to a clause containing lit S->DB[mem] = S->first[lit]; S->first[lit] = mem; } // By updating the database and the pointers int* getMemory (struct solver* S, int mem_size) { // Allocate memory of size mem_size if (S->mem_used + mem_size > S->mem_max) { // In case the code is used within a code base printf ("c out of memory\n"); exit (0); } int *store = (S->DB + S->mem_used); // Compute a pointer to the new memory location S->mem_used += mem_size; // Update the size of the used memory return store; } // Return the pointer int* addClause (struct solver* S, int* in, int size, int irr) { // Adds a clause stored in *in of size size int i, used = S->mem_used; // Store a pointer to the beginning of the clause int* clause = getMemory (S, size + 3) + 2; // Allocate memory for the clause in the database if (size > 1) { addWatch (S, in[0], used ); // If the clause is not unit, then add addWatch (S, in[1], used+1); } // Two watch pointers to the datastructure for (i = 0; i < size; i++) clause[i] = in[i]; clause[i] = 0; // Copy the clause from the buffer to the database if (irr) S->mem_fixed = S->mem_used; else S->nLemmas++; // Update the statistics return clause; } // Return the pointer to the clause in the database void reduceDB (struct solver* S, int k) { // Removes "less useful" lemmas from DB while (S->nLemmas > S->maxLemmas) S->maxLemmas += 300; // Allow more lemmas in the future S->nLemmas = 0; // Reset the number of lemmas int i; for (i = -S->nVars; i <= S->nVars; i++) { // Loop over the variables if (i == 0) continue; int* watch = &S->first[i]; // Get the pointer to the first watched clause while (*watch != END) // As long as there are watched clauses if (*watch < S->mem_fixed) watch = (S->DB + *watch); // Remove the watch if it points to a lemma else *watch = S->DB[ *watch]; } // Otherwise (meaning an input clause) go to next watch int old_used = S->mem_used; S->mem_used = S->mem_fixed; // Virtually remove all lemmas for (i = S->mem_fixed + 2; i < old_used; i += 3) { // While the old memory contains lemmas int count = 0, head = i; // Get the lemma to which the head is pointing while (S->DB[i]) { int lit = S->DB[i++]; // Count the number of literals if ((lit > 0) == S->model[abs (lit)]) count++; } // That are satisfied by the current model if (count < k) addClause (S, S->DB+head, i-head, 0); } } // If the latter is smaller than k, add it back void bump (struct solver* S, int lit) { // Move the variable to the front of the decision list if (S->msfalse[lit] != IMPLIED) { S->msfalse[lit] = MARK; // MARK the literal as involved if not a top-level unit int var = abs (lit); if (var != S->head) { // In case var is not already the head of the list S->prev[S->next[var]] = S->prev[var]; // Update the prev link, and S->next[S->prev[var]] = S->next[var]; // Update the next link, and S->next[S->head] = var; // Add a next link to the head, and S->prev[var] = S->head; S->head = var; } } } // Make var the new head int implied (struct solver* S, int lit) { // Check if lit(eral) is implied by MARK literals if (S->msfalse[lit] > MARK) return (S->msfalse[lit] & MARK); // If checked before return old result if (!S->reason[abs (lit)]) return 0; // In case lit is a decision, it is not implied int* p = (S->DB + S->reason[abs (lit)] - 1); // Get the reason of lit(eral) while (*(++p)) // While there are literals in the reason if ((S->msfalse[*p] ^ MARK) && !implied (S, *p)) { // Recursively check if non-MARK literals are implied S->msfalse[lit] = IMPLIED - 1; return 0; } // Mark and return not implied (denoted by IMPLIED - 1) S->msfalse[lit] = IMPLIED; return 1; } // Mark and return that the literal is implied int* analyze (struct solver* S, int* clause) { // Compute a resolvent from falsified clause S->res++; S->nConflicts++; // Bump restarts and update the statistic while (*clause) bump (S, *(clause++)); // MARK all literals in the falsified clause while (S->reason[abs (*(--S->assigned))]) { // Loop on variables on falseStack until the last decision if (S->msfalse[*S->assigned] == MARK) { // If the tail of the stack is MARK int *check = S->assigned; // Pointer to check if first-UIP is reached while (S->msfalse[*(--check)] != MARK) // Check for a MARK literal before decision if (!S->reason[abs(*check)]) goto build; // Otherwise it is the first-UIP so break clause = S->DB + S->reason[abs (*S->assigned)]; // Get the reason and ignore first literal while (*clause) bump (S, *(clause++)); } // MARK all literals in reason unassign (S, *S->assigned); } // Unassign the tail of the stack build:; int size = 0, lbd = 0, flag = 0; // Build conflict clause; Empty the clause buffer int* p = S->processed = S->assigned; // Loop from tail to front while (p >= S->forced) { // Only literals on the stack can be MARKed if ((S->msfalse[*p] == MARK) && !implied (S, *p)) { // If MARKed and not implied S->buffer[size++] = *p; flag = 1; } // Add literal to conflict clause buffer if (!S->reason[abs (*p)]) { lbd += flag; flag = 0; // Increase LBD for a decision with a true flag if (size == 1) S->processed = p; } // And update the processed pointer S->msfalse[*(p--)] = 1; } // Reset the MARK flag for all variables on the stack S->fast -= S->fast >> 5; S->fast += lbd << 15; // Update the fast moving average S->slow -= S->slow >> 15; S->slow += lbd << 5; // Update the slow moving average while (S->assigned > S->processed) // Loop over all unprocessed literals unassign (S, *(S->assigned--)); // Unassign all lits between tail & head unassign (S, *S->assigned); // Assigned now equal to processed S->buffer[size] = 0; // Terminate the buffer (and potentially print clause) return addClause (S, S->buffer, size, 0); } // Add new conflict clause to redundant DB int propagate (struct solver* S) { // Performs unit propagation int forced = S->reason[abs (*S->processed)]; // Initialize forced flag while (S->processed < S->assigned) { // While unprocessed false literals int lit = *(S->processed++); // Get first unprocessed literal int* watch = &S->first[lit]; // Obtain the first watch pointer while (*watch != END) { // While there are watched clauses (watched by lit) int i, unit = 1; // Let's assume that the clause is unit int* clause = (S->DB + *watch + 1); // Get the clause from DB if (clause[-2] == 0) clause++; // Set the pointer to the first literal in the clause if (clause[ 0] == lit) clause[0] = clause[1]; // Ensure that the other watched literal is in front for (i = 2; unit && clause[i]; i++) // Scan the non-watched literals if (!S->msfalse[clause[i]]) { // When clause[i] is not false, it is either true or unset clause[1] = clause[i]; clause[i] = lit; // Swap literals int store = *watch; unit = 0; // Store the old watch *watch = S->DB[*watch]; // Remove the watch from the list of lit addWatch (S, clause[1], store); } // Add the watch to the list of clause[1] if (unit) { // If the clause is indeed unit clause[1] = lit; watch = (S->DB + *watch); // Place lit at clause[1] and update next watch if ( S->msfalse[-clause[0]]) continue; // If the other watched literal is satisfied continue if (!S->msfalse[ clause[0]]) { // If the other watched literal is falsified, assign (S, clause, forced); } // A unit clause is found, and the reason is set else { if (forced) return UNSAT; // Found a root level conflict -> UNSAT int* lemma = analyze (S, clause); // Analyze the conflict return a conflict clause if (!lemma[1]) forced = 1; // In case a unit clause is found, set forced flag assign (S, lemma, forced); break; } } } } // Assign the conflict clause as a unit if (forced) S->forced = S->processed; // Set S->forced if applicable return SAT; } // Finally, no conflict was found int solve (struct solver* S) { // Determine satisfiability int decision = S->head; S->res = 0; // Initialize the solver for (;;) { // Main solve loop int old_nLemmas = S->nLemmas; // Store nLemmas to see whether propagate adds lemmas if (propagate (S) == UNSAT) return UNSAT; // Propagation returns UNSAT for a root level conflict if (S->nLemmas > old_nLemmas) { // If the last decision caused a conflict decision = S->head; // Reset the decision heuristic to head if (S->fast > (S->slow / 100) * 125) { // If fast average is substantially larger than slow average // printf("c restarting after %i conflicts (%i %i) %i\n", S->res, S->fast, S->slow, S->nLemmas > S->maxLemmas); S->res = 0; S->fast = (S->slow / 100) * 125; restart (S); // Restart and update the averages if (S->nLemmas > S->maxLemmas) reduceDB (S, 6); } } // Reduce the DB when it contains too many lemmas while (S->msfalse[decision] || S->msfalse[-decision]) { // As long as the temporay decision is assigned decision = S->prev[decision]; } // Replace it with the next variable in the decision list if (decision == 0) return SAT; // If the end of the list is reached, then a solution is found decision = S->model[decision] ? decision : -decision; // Otherwise, assign the decision variable based on the model S->msfalse[-decision] = 1; // Assign the decision literal to true (change to IMPLIED-1?) *(S->assigned++) = -decision; // And push it on the assigned stack decision = abs(decision); S->reason[decision] = 0; } } // Decisions have no reason clauses void initCDCL (struct solver* S, int n, int m) { if (n < 1) n = 1; // The code assumes that there is at least one variable S->nVars = n; // Set the number of variables S->nClauses = m; // Set the number of clauses S->mem_max = 1 << 27; // Set the initial maximum memory S->mem_used = 0; // The number of integers allocated in the DB S->nLemmas = 0; // The number of learned clauses -- redundant means learned S->nConflicts = 0; // Number of conflicts used to update scores S->maxLemmas = 2000; // Initial maximum number of learned clauses S->fast = S->slow = 1 << 24; // Initialize the fast and slow moving averages S->DB = (int *) calloc (sizeof (int), S->mem_max); // Allocate the initial database S->model = getMemory (S, n+1); // Full assignment of the (Boolean) variables (initially set to false) S->next = getMemory (S, n+1); // Next variable in the heuristic order S->prev = getMemory (S, n+1); // Previous variable in the heuristic order S->buffer = getMemory (S, n ); // A buffer to store a temporary clause S->reason = getMemory (S, n+1); // Array of clauses S->falseStack = getMemory (S, n+1); // Stack of falsified literals -- this pointer is never changed S->forced = S->falseStack; // Points inside *falseStack at first decision (unforced literal) S->processed = S->falseStack; // Points inside *falseStack at first unprocessed literal S->assigned = S->falseStack; // Points inside *falseStack at last unprocessed literal S->msfalse = getMemory (S, 2*n+1); S->msfalse += n; // Labels for variables, non-zero means false S->first = getMemory (S, 2*n+1); S->first += n; // Offset of the first watched clause S->DB[S->mem_used++] = 0; // Make sure there is a 0 before the clauses are loaded. int i; for (i = 1; i <= n; i++) { // Initialize the main datastructures: S->prev [i] = i - 1; S->next[i-1] = i; // the double-linked list for variable-move-to-front, S->model[i] = S->msfalse[-i] = S->msfalse[i] = 0; // the model (phase-saving), the false array, S->first[i] = S->first[-i] = END; } // and first (watch pointers). S->head = n; } // Initialize the head of the double-linked list /* end microsat */ struct ed { int b, spec, id ; } ; vector> edges ; vector isspec ; int n, m, k ; int symc ; int gensym() { return symc++ ; } vector> problem ; const int TRUE = 1000000000 ; const int FALSE = -TRUE ; int addclause(vector &v) { for (int i=0; i<(int)v.size(); i++) if (v[i] == TRUE) return SAT ; for (int i=(int)v.size()-1; i>=0; i--) if (v[i] == FALSE) { swap(v[i], v[v.size()-1]) ; v.pop_back() ; } if (v.size() == 0) return SAT ; problem.push_back(v) ; return SAT ; } int addclause(int c0) { vector v({c0}) ; return addclause(v) ; } int addclause(int c0, int c1) { vector v({c0, c1}) ; return addclause(v) ; } int addclause(int c0, int c1, int c2) { vector v({c0, c1, c2}) ; return addclause(v) ; } int main() { cin >> n >> m >> k ; isspec.resize(n) ; edges.resize(n) ; for (int i=0; i> a >> b ; int s = (i < k) ; a-- ; b-- ; edges[a].push_back({b,s,i+1}) ; edges[b].push_back({a,s,i+1}) ; if (s) { isspec[a]++ ; isspec[b]++ ; } } symc = m+1 ; for (int i=0; i iota ; for (int i=1; i<=m; i++) iota.push_back(i) ; addclause(iota) ; struct solver S; // Create the solver datastructure S.nVars = symc - 1 ; S.nClauses = problem.size() ; initCDCL(&S, S.nVars, S.nClauses); // Allocate the main datastructures int r = END ; for (auto v: problem) { int size = v.size() ; int* clause = addClause(&S, v.data(), size, 1); // Then add the clause to data_base if (!size || ((size == 1) && S.msfalse[clause[0]])) { // Check for empty clause or conflicting unit r = -1; // If either is found return UNSAT break ; } if ((size == 1) && !S.msfalse[-clause[0]]) { // Check for a new unit assign(&S, clause, 1); } // Directly assign new units (forced = 1) } if (r == END) r = solve(&S) ; if (m == 0 || r == UNSAT) { cout << -1 << endl ; } else if (r == SAT) { vector cyc ; vector vis(n) ; int aa=-1, bb=-1 ; for (int i=0; aa<0 && i