Pages that link to "Item:Q5621961"
From MaRDI portal
The following pages link to A machine program for theorem-proving (Q5621961):
Displaying 50 items.
- MaxMinMax problem and sparse equations over finite fields (Q285259) (← links)
- Interpolation systems for ground proofs in automated deduction: a survey (Q287275) (← links)
- Semantically-guided goal-sensitive reasoning: model representation (Q287333) (← links)
- An experiment with satisfiability modulo SAT (Q287334) (← links)
- An integer programming approach to the multimode resource-constrained multiproject scheduling problem (Q310345) (← links)
- An approach using SAT solvers for the RCPSP with logical constraints (Q321002) (← links)
- Stochastic enumeration method for counting NP-hard problems (Q352890) (← links)
- Planning as satisfiability: heuristics (Q359984) (← links)
- A SAT-based preimage analysis of reduced \textsc{Keccak} hash functions (Q396606) (← links)
- On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\) (Q400514) (← links)
- Decomposition representations of logical equations in problems of inversion of discrete functions (Q404200) (← links)
- Towards NP-P via proof complexity and search (Q408544) (← links)
- A numerical method for Lane-Emden equations using hybrid functions and the collocation method (Q410929) (← links)
- Finding kernels or solving SAT (Q414435) (← links)
- Creating non-minimal triangulations for use in inference in mixed stochastic/deterministic graphical models (Q415616) (← links)
- Computing weighted solutions in ASP: representation-based method vs. search-based method (Q421455) (← links)
- Multi-mode resource-constrained project scheduling using RCPSP and SAT solvers (Q421579) (← links)
- Learning from conflicts in propositional satisfiability (Q427560) (← links)
- A pearl on SAT and SMT solving in Prolog (Q428887) (← links)
- Model evolution with equality -- revised and implemented (Q429586) (← links)
- Toward a model for backtracking and dynamic programming (Q430838) (← links)
- Combining decision procedures by (model-)equality propagation (Q436376) (← links)
- A note on SAT algorithms and proof complexity (Q436581) (← links)
- On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
- An instantiation scheme for satisfiability modulo theories (Q438578) (← links)
- Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search (Q457253) (← links)
- Automatic verification of reduction techniques in higher order logic (Q469363) (← links)
- Bernstein series solution of a class of Lane-Emden type equations (Q473647) (← links)
- Curriculum-based course timetabling with SAT and MaxSAT (Q475170) (← links)
- Quantifier elimination by dependency sequents (Q479823) (← links)
- Deciding floating-point logic with abstract conflict driven clause learning (Q479837) (← links)
- An overview of parallel SAT solving (Q487635) (← links)
- Relating constraint answer set programming languages and algorithms (Q490456) (← links)
- Finding rough and fuzzy-rough set reducts with SAT (Q497893) (← links)
- CCEHC: an efficient local search algorithm for weighted partial maximum satisfiability (Q502391) (← links)
- Two approximate algorithms for model counting (Q507433) (← links)
- Improving configuration checking for satisfiable random \(k\)-SAT instances (Q513324) (← links)
- A search-based procedure for nonlinear real arithmetic (Q518407) (← links)
- Cardinality networks: a theoretical and empirical study (Q538318) (← links)
- John McCarthy's legacy (Q543573) (← links)
- On the power of clause-learning SAT solvers as resolution engines (Q543613) (← links)
- Leveraging belief propagation, backtrack search, and statistics for model counting (Q545553) (← links)
- Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances (Q596103) (← links)
- A weight-balanced branching rule for SAT (Q597527) (← links)
- Solving satisfiability problems with preferences (Q606909) (← links)
- Formal verification of a modern SAT solver by shallow embedding into Isabelle/HOL (Q606999) (← links)
- A randomized algorithm for 3-SAT (Q626900) (← links)
- Explaining the \texttt{cumulative} propagator (Q647477) (← links)
- Matroid enumeration for incidence geometry (Q664549) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
